Hets - the Heterogeneous Tool Set
Copyright(c) University of Cambridge Cambridge England
adaption (c) Till Mossakowski Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Isabelle.IsaProve

Description

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) () Source #

isabelleBatchProver :: Prover Sign Sentence (DefaultMorphism Sign) () () Source #

isabelleProver :: IsaEditor -> Prover Sign Sentence (DefaultMorphism Sign) () () Source #

data IsaEditor Source #

Constructors

Emacs 
JEdit 

Instances

Instances details
Show IsaEditor Source # 
Instance details

Defined in Isabelle.IsaProve

Methods

showsPrec :: Int -> IsaEditor -> ShowS

show :: IsaEditor -> String

showList :: [IsaEditor] -> ShowS

isaProve :: IsaEditor -> String -> Theory Sign Sentence () -> a -> IO [ProofStatus ()] Source #