Copyright	(c) Jonathan von Schroeder, DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	jonathan.von_schroeder@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred

HolLight.Sentence

Description

Definition of sentences for HolLight logic

Ref.

Documentation

Constructors

Sentence
Fields term :: Term proof :: Maybe HolProof

Instances

Eq Sentence
Data Sentence
Ord Sentence
Show Sentence
ShATermConvertible Sentence
GetRange Sentence
Pretty Sentence
Typeable * Sentence
MinSublogic HolLightSL Sentence
Sentences HolLight Sentence Sign HolLightMorphism ()
StaticAnalysis HolLight () Sentence () () Sign HolLightMorphism () ()	Static Analysis for propositional logic
Logic HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () ()	Instance of Logic for propositional logc
Comorphism HolLight2Isabelle HolLight HolLightSL () Sentence () () Sign HolLightMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()