Source : Free On-Line Dictionary of Computing

Isabelle
     
         A generic {theorem prover} with support for
        several {object-logics}, developed by Lawrence C. Paulson
         in collaboration with {Tobias
        Nipkow (http://www.in.tum.de/~nipkow/)} at the {Technical
        University of Munich}.
     
        A system of {type classes} allows {polymorphic} object-logics
        with {overloading} and automatic {type inference}.
     
        Isabelle supports {first-order logic} - {constructive} and
        classical versions; {higher-order logic}, similar to Gordon's
        {HOL}; {Zermelo Frankel set theory}; an {extensional} version
        of {Martin Lof}'s {type theory}, the classical first-order
        {sequent calculus}, {LK}; the {modal logics} {T}, {S4}, and
        {S43}; and {Logic for Computable Functions}.
     
        An object logic's {syntax} and {inference rules} are specified
        {declaratively} allowing single-step proof construction.
        {Proof procedures} can be expressed using "tactics" and
        "tacticals".  Isabelle provides control structures for
        expressing search procedures and generic tools such as
        simplifiers and classical theorem provers which can be applied
        to object-logics.  Isabelle is built on top of {Standard ML}
        and uses its user interface.
     
        {Home (http://www.cl.cam.ac.uk/Research/HVG/Isabelle/)}.
     
        Mailing list: [email protected].
     
        ["tactics"?  "tacticals"?]
     
        (1999-07-26)