Copyright | (c) University of Cambridge, Cambridge, England adaption (c) Till Mossakowski, Uni Bremen 2002-2005 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Interface for Isabelle theorem prover. Interface between Isabelle and Hets: Hets writes Isabelle .thy file and starts Isabelle User extends .thy file with proofs User finishes Isabelle Hets reads in created *.deps files
Documentation
isabelleConsChecker :: ConsChecker Sign Sentence () (DefaultMorphism Sign) ()
isabelleBatchProver :: Prover Sign Sentence (DefaultMorphism Sign) () ()
isabelleProver :: Prover Sign Sentence (DefaultMorphism Sign) () ()