| Copyright | (c) Jonathan von Schroeder, DFKI GmbH 2010 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | jonathan.von_schroeder@dfki.de |
| Stability | experimental |
| Portability | non-portable (imports Logic.Logic) |
| Safe Haskell | None |
HolLight.Logic_HolLight
Description
Instance of class Logic for HolLight logic Also the instances for Syntax and Category.
Ref.
- type HolLightMorphism = DefaultMorphism Sign
- data HolLight = HolLight
Documentation
type HolLightMorphism = DefaultMorphism Sign
data HolLight
Lid for HolLight logic
Constructors
| HolLight |
Instances
| Show HolLight | |
| Language HolLight | |
| Sentences HolLight Sentence Sign HolLightMorphism () | |
| Syntax HolLight () () () () | |
| 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 () () () |