Safe Haskell	None

Isabelle.IsaExport

Documentation

newtype Export

Constructors

Export (List1 Thy)

Instances

Eq Export
Show Export
XmlContent Export
HTypeable Export

data Thy

Constructors

Thy Thy_Attrs (List1 Import) [Keyword] [UseFile] Body

Instances

Eq Thy
Show Thy
XmlContent Thy
HTypeable Thy

data Thy_Attrs

Constructors

Thy_Attrs
Fields thyName :: String thyHeader :: Maybe String

Instances

Eq Thy_Attrs
Show Thy_Attrs
XmlAttributes Thy_Attrs

data Keyword

Constructors

Keyword
Fields keywordName :: String

Instances

Eq Keyword
Show Keyword
XmlContent Keyword
XmlAttributes Keyword
HTypeable Keyword

data Import

Constructors

Import
Fields importName :: String

Instances

Eq Import
Show Import
XmlContent Import
XmlAttributes Import
HTypeable Import

data UseFile

Constructors

UseFile
Fields useFileName :: String

Instances

Eq UseFile
Show UseFile
XmlContent UseFile
XmlAttributes UseFile
HTypeable UseFile

newtype Body

Constructors

Body [Body_]

Instances

Eq Body
Show Body
XmlContent Body
HTypeable Body

data Locale

Constructors

Locale Locale_Attrs Ctxt [Parent] Body

Instances

Eq Locale
Show Locale
XmlContent Locale
HTypeable Locale

data Locale_Attrs

Constructors

Locale_Attrs
Fields localeName :: String

Instances

Eq Locale_Attrs
Show Locale_Attrs
XmlAttributes Locale_Attrs

data Cls

Constructors

Cls Cls_Attrs Ctxt [Parent] Body

Instances

Eq Cls
Show Cls
XmlContent Cls
HTypeable Cls

data Cls_Attrs

Constructors

Cls_Attrs
Fields clsName :: String

Instances

Eq Cls_Attrs
Show Cls_Attrs
XmlAttributes Cls_Attrs

data TypeSynonym

Constructors

TypeSynonym TypeSynonym_Attrs (Maybe Mixfix) Vars (OneOf3 TVar TFree Type)

Instances

Eq TypeSynonym
Show TypeSynonym
XmlContent TypeSynonym
HTypeable TypeSynonym

data TypeSynonym_Attrs

Constructors

TypeSynonym_Attrs
Fields typeSynonymName :: String typeSynonymTarget :: Maybe String

Instances

Eq TypeSynonym_Attrs
Show TypeSynonym_Attrs
XmlAttributes TypeSynonym_Attrs

newtype Datatypes

Constructors

Datatypes (List1 Datatype)

Instances

Eq Datatypes
Show Datatypes
XmlContent Datatypes
HTypeable Datatypes

data Datatype

Constructors

Datatype Datatype_Attrs (Maybe Mixfix) (List1 Constructor) [TFree]

Instances

Eq Datatype
Show Datatype
XmlContent Datatype
HTypeable Datatype

data Datatype_Attrs

Constructors

Datatype_Attrs
Fields datatypeName :: String

Instances

Eq Datatype_Attrs
Show Datatype_Attrs
XmlAttributes Datatype_Attrs

data Constructor

Constructors

Constructor Constructor_Attrs (Maybe Mixfix) (OneOf3 TVar TFree Type) [OneOf3 TVar TFree Type]

Instances

Eq Constructor
Show Constructor
XmlContent Constructor
HTypeable Constructor

data Constructor_Attrs

Constructors

Constructor_Attrs
Fields constructorName :: Maybe String

Instances

Eq Constructor_Attrs
Show Constructor_Attrs
XmlAttributes Constructor_Attrs

newtype Domains

Constructors

Domains (List1 Domain)

Instances

Eq Domains
Show Domains
XmlContent Domains
HTypeable Domains

data Domain

Constructors

Domain Domain_Attrs (Maybe Mixfix) [TFree] (List1 DomainConstructor)

Instances

Eq Domain
Show Domain
XmlContent Domain
HTypeable Domain

data Domain_Attrs

Constructors

Domain_Attrs
Fields domainName :: String

Instances

Eq Domain_Attrs
Show Domain_Attrs
XmlAttributes Domain_Attrs

data DomainConstructor

Constructors

DomainConstructor DomainConstructor_Attrs (OneOf3 TVar TFree Type) [DomainConstructorArg]

Instances

Eq DomainConstructor
Show DomainConstructor
XmlContent DomainConstructor
HTypeable DomainConstructor

data DomainConstructor_Attrs

Constructors

DomainConstructor_Attrs
Fields domainConstructorName :: String

Instances

Eq DomainConstructor_Attrs
Show DomainConstructor_Attrs
XmlAttributes DomainConstructor_Attrs

data DomainConstructorArg

Constructors

DomainConstructorArg DomainConstructorArg_Attrs (OneOf3 TVar TFree Type)

Instances

Eq DomainConstructorArg
Show DomainConstructorArg
XmlContent DomainConstructorArg
HTypeable DomainConstructorArg

data DomainConstructorArg_Attrs

Constructors

DomainConstructorArg_Attrs
Fields domainConstructorArgLazy :: Maybe String domainConstructorArgName :: Maybe String

Instances

Eq DomainConstructorArg_Attrs
Show DomainConstructorArg_Attrs
XmlAttributes DomainConstructorArg_Attrs

newtype Consts

Constructors

Consts (List1 ConstDef)

Instances

Eq Consts
Show Consts
XmlContent Consts
HTypeable Consts

data ConstDef

Constructors

ConstDef ConstDef_Attrs (Maybe Mixfix) (OneOf3 TVar TFree Type)

Instances

Eq ConstDef
Show ConstDef
XmlContent ConstDef
HTypeable ConstDef

data ConstDef_Attrs

Constructors

ConstDef_Attrs
Fields constDefName :: String

Instances

Eq ConstDef_Attrs
Show ConstDef_Attrs
XmlAttributes ConstDef_Attrs

newtype Axioms

Constructors

Axioms (List1 Axiom)

Instances

Eq Axioms
Show Axioms
XmlContent Axioms
HTypeable Axioms

data Axiom

Constructors

Axiom Axiom_Attrs (OneOf6 Bound Free Var Const App Abs)

Instances

Eq Axiom
Show Axiom
XmlContent Axiom
HTypeable Axiom

data Axiom_Attrs

Constructors

Axiom_Attrs
Fields axiomName :: String axiomArgs :: String

Instances

Eq Axiom_Attrs
Show Axiom_Attrs
XmlAttributes Axiom_Attrs

data Lemma

Constructors

Lemma Lemma_Attrs Ctxt Proof (List1 Shows)

Instances

Eq Lemma
Show Lemma
XmlContent Lemma
HTypeable Lemma

data Lemma_Attrs

Constructors

Lemma_Attrs
Fields lemmaTarget :: Maybe String

Instances

Eq Lemma_Attrs
Show Lemma_Attrs
XmlAttributes Lemma_Attrs

data Definition

Constructors

Definition Definition_Attrs (Maybe Mixfix) (OneOf3 TVar TFree Type) (List1 (OneOf6 Bound Free Var Const App Abs))

Instances

Eq Definition
Show Definition
XmlContent Definition
HTypeable Definition

data Definition_Attrs

Constructors

Definition_Attrs
Fields definitionName :: String definitionTarget :: Maybe String

Instances

Eq Definition_Attrs
Show Definition_Attrs
XmlAttributes Definition_Attrs

data Funs

Constructors

Funs Funs_Attrs (List1 Fun)

Instances

Eq Funs
Show Funs
XmlContent Funs
HTypeable Funs

data Funs_Attrs

Constructors

Funs_Attrs
Fields funsTarget :: Maybe String funsSequential :: Maybe String funsDefault :: Maybe String funsDomintros :: Maybe String funsPartials :: Maybe String

Instances

Eq Funs_Attrs
Show Funs_Attrs
XmlAttributes Funs_Attrs

data Fun

Constructors

Fun Fun_Attrs (Maybe Mixfix) (OneOf3 TVar TFree Type) (List1 Equation)

Instances

Eq Fun
Show Fun
XmlContent Fun
HTypeable Fun

data Fun_Attrs

Constructors

Fun_Attrs
Fields funName :: String

Instances

Eq Fun_Attrs
Show Fun_Attrs
XmlAttributes Fun_Attrs

newtype Equation

Constructors

Equation (List1 (OneOf6 Bound Free Var Const App Abs))

Instances

Eq Equation
Show Equation
XmlContent Equation
HTypeable Equation

data Primrec

Constructors

Primrec Primrec_Attrs (List1 Fun)

Instances

Eq Primrec
Show Primrec
XmlContent Primrec
HTypeable Primrec

data Primrec_Attrs

Constructors

Primrec_Attrs
Fields primrecTarget :: Maybe String

Instances

Eq Primrec_Attrs
Show Primrec_Attrs
XmlAttributes Primrec_Attrs

newtype Fixrec

Constructors

Fixrec (List1 FixrecFun)

Instances

Eq Fixrec
Show Fixrec
XmlContent Fixrec
HTypeable Fixrec

data FixrecFun

Constructors

FixrecFun FixrecFun_Attrs (Maybe Mixfix) (OneOf3 TVar TFree Type) (List1 FixrecEquation)

Instances

Eq FixrecFun
Show FixrecFun
XmlContent FixrecFun
HTypeable FixrecFun

data FixrecFun_Attrs

Constructors

FixrecFun_Attrs
Fields fixrecFunName :: String

Instances

Eq FixrecFun_Attrs
Show FixrecFun_Attrs
XmlAttributes FixrecFun_Attrs

data FixrecEquation

Constructors

FixrecEquation FixrecEquation_Attrs Premises (List1 (OneOf6 Bound Free Var Const App Abs))

Instances

Eq FixrecEquation
Show FixrecEquation
XmlContent FixrecEquation
HTypeable FixrecEquation

data FixrecEquation_Attrs

Constructors

FixrecEquation_Attrs
Fields fixrecEquationUnchecked :: Maybe String

Instances

Eq FixrecEquation_Attrs
Show FixrecEquation_Attrs
XmlAttributes FixrecEquation_Attrs

newtype Premises

Constructors

Premises [OneOf6 Bound Free Var Const App Abs]

Instances

Eq Premises
Show Premises
XmlContent Premises
HTypeable Premises

data Instantiation

Constructors

Instantiation Instantiation_Attrs Arity Body

Instances

Eq Instantiation
Show Instantiation
XmlContent Instantiation
HTypeable Instantiation

data Instantiation_Attrs

Constructors

Instantiation_Attrs
Fields instantiationType :: String

Instances

Eq Instantiation_Attrs
Show Instantiation_Attrs
XmlAttributes Instantiation_Attrs

data Instance

Constructors

Instance Instance_Attrs Proof (Maybe (Vars, Arity))

Instances

Eq Instance
Show Instance
XmlContent Instance
HTypeable Instance

data Instance_Attrs

Constructors

Instance_Attrs
Fields instanceClass :: Maybe String instanceRel :: Maybe String instanceClass1 :: Maybe String

Instances

Eq Instance_Attrs
Show Instance_Attrs
XmlAttributes Instance_Attrs

data Subclass

Constructors

Subclass Subclass_Attrs Proof

Instances

Eq Subclass
Show Subclass
XmlContent Subclass
HTypeable Subclass

data Subclass_Attrs

Constructors

Subclass_Attrs
Fields subclassClass :: String subclassTarget :: Maybe String

Instances

Eq Subclass_Attrs
Show Subclass_Attrs
XmlAttributes Subclass_Attrs

data Typedef

Constructors

Typedef Typedef_Attrs (Maybe Mixfix) Proof (OneOf6 Bound Free Var Const App Abs) [TFree]

Instances

Eq Typedef
Show Typedef
XmlContent Typedef
HTypeable Typedef

data Typedef_Attrs

Constructors

Typedef_Attrs
Fields typedefType :: String typedefM1 :: Maybe String typedefM2 :: Maybe String

Instances

Eq Typedef_Attrs
Show Typedef_Attrs
XmlAttributes Typedef_Attrs

data Defs

Constructors

Defs Defs_Attrs (List1 Def)

Instances

Eq Defs
Show Defs
XmlContent Defs
HTypeable Defs

data Defs_Attrs

Constructors

Defs_Attrs
Fields defsUnchecked :: Maybe String defsOverloaded :: Maybe String

Instances

Eq Defs_Attrs
Show Defs_Attrs
XmlAttributes Defs_Attrs

data Def

Constructors

Def Def_Attrs (OneOf3 TVar TFree Type) (OneOf6 Bound Free Var Const App Abs)

Instances

Eq Def
Show Def
XmlContent Def
HTypeable Def

data Def_Attrs

Constructors

Def_Attrs
Fields defName :: String defArgs :: String defConst :: String

Instances

Eq Def_Attrs
Show Def_Attrs
XmlAttributes Def_Attrs

newtype Sort

Constructors

Sort (List1 Class)

Instances

Eq Sort
Show Sort
XmlContent Sort
HTypeable Sort

data Arity

Constructors

Arity Sort [Sort]

Instances

Eq Arity
Show Arity
XmlContent Arity
HTypeable Arity

newtype Vars

Constructors

Vars [TFree]

Instances

Eq Vars
Show Vars
XmlContent Vars
HTypeable Vars

data Parent

Constructors

Parent
Fields parentName :: String

Instances

Eq Parent
Show Parent
XmlContent Parent
XmlAttributes Parent
HTypeable Parent

newtype Fixes

Constructors

Fixes [Fix]

Instances

Eq Fixes
Show Fixes
XmlContent Fixes
HTypeable Fixes

data Fix

Constructors

Fix Fix_Attrs (OneOf3 TVar TFree Type) (Maybe Mixfix)

Instances

Eq Fix
Show Fix
XmlContent Fix
HTypeable Fix

data Fix_Attrs

Constructors

Fix_Attrs
Fields fixName :: String

Instances

Eq Fix_Attrs
Show Fix_Attrs
XmlAttributes Fix_Attrs

newtype Assumes

Constructors

Assumes [Assumption]

Instances

Eq Assumes
Show Assumes
XmlContent Assumes
HTypeable Assumes

data Assumption

Constructors

Assumption Assumption_Attrs (OneOf6 Bound Free Var Const App Abs)

Instances

Eq Assumption
Show Assumption
XmlContent Assumption
HTypeable Assumption

data Assumption_Attrs

Constructors

Assumption_Attrs
Fields assumptionName :: String assumptionArgs :: String

Instances

Eq Assumption_Attrs
Show Assumption_Attrs
XmlAttributes Assumption_Attrs

newtype Ctxt

Constructors

Ctxt [OneOf2 Fixes Assumes]

Instances

Eq Ctxt
Show Ctxt
XmlContent Ctxt
HTypeable Ctxt

data Mixfix

Constructors

Mixfix Mixfix_Attrs [OneOf4 Arg AString Break Block]

Instances

Eq Mixfix
Show Mixfix
XmlContent Mixfix
HTypeable Mixfix

data Mixfix_Attrs

Constructors

Mixfix_Attrs
Fields mixfixNargs :: String mixfixPrio :: String mixfixPretty :: String

Instances

Eq Mixfix_Attrs
Show Mixfix_Attrs
XmlAttributes Mixfix_Attrs

data Arg

Constructors

Arg
Fields argPrio :: String

Instances

Eq Arg
Show Arg
XmlContent Arg
XmlAttributes Arg
HTypeable Arg

data AString

Constructors

AString
Fields stringVal :: String

Instances

Eq AString
Show AString
XmlContent AString
XmlAttributes AString
HTypeable AString

data Break

Constructors

Break
Fields breakPrio :: String

Instances

Eq Break
Show Break
XmlContent Break
XmlAttributes Break
HTypeable Break

data Block

Constructors

Block Block_Attrs [OneOf4 Arg AString Break Block]

Instances

Eq Block
Show Block
XmlContent Block
HTypeable Block

data Block_Attrs

Constructors

Block_Attrs
Fields blockPrio :: String

Instances

Eq Block_Attrs
Show Block_Attrs
XmlAttributes Block_Attrs

newtype Proof

Constructors

Proof String

Instances

Eq Proof
Show Proof
XmlContent Proof
HTypeable Proof

data Shows

Constructors

Shows Shows_Attrs (List1 AShow)

Instances

Eq Shows
Show Shows
XmlContent Shows
HTypeable Shows

data Shows_Attrs

Constructors

Shows_Attrs
Fields showsName :: String showsArgs :: Maybe String

Instances

Eq Shows_Attrs
Show Shows_Attrs
XmlAttributes Shows_Attrs

newtype AShow

Constructors

AShow (List1 (OneOf6 Bound Free Var Const App Abs))

Instances

Eq AShow
Show AShow
XmlContent AShow
HTypeable AShow

data Bound

Constructors

Bound
Fields boundIndex :: String

Instances

Eq Bound
Show Bound
XmlContent Bound
XmlAttributes Bound
HTypeable Bound

data Free

Constructors

FreeTVar Free_Attrs TVar
FreeTFree Free_Attrs TFree
FreeType Free_Attrs Type

Instances

Eq Free
Show Free
XmlContent Free
HTypeable Free

data Free_Attrs

Constructors

Free_Attrs
Fields freeName :: String

Instances

Eq Free_Attrs
Show Free_Attrs
XmlAttributes Free_Attrs

data Var

Constructors

VarTVar Var_Attrs TVar
VarTFree Var_Attrs TFree
VarType Var_Attrs Type

Instances

Eq Var
Show Var
XmlContent Var
HTypeable Var

data Var_Attrs

Constructors

Var_Attrs
Fields varName :: String varIndex :: Maybe String

Instances

Eq Var_Attrs
Show Var_Attrs
XmlAttributes Var_Attrs

data Const

Constructors

Const Const_Attrs (OneOf3 TVar TFree Type)

Instances

Eq Const
Show Const
XmlContent Const
HTypeable Const

data Const_Attrs

Constructors

Const_Attrs
Fields constName :: String

Instances

Eq Const_Attrs
Show Const_Attrs
XmlAttributes Const_Attrs

data App

Constructors

App (OneOf6 Bound Free Var Const App Abs) (OneOf6 Bound Free Var Const App Abs)

Instances

Eq App
Show App
XmlContent App
HTypeable App

data Abs

Constructors

Abs Abs_Attrs (OneOf3 TVar TFree Type) (OneOf6 Bound Free Var Const App Abs)

Instances

Eq Abs
Show Abs
XmlContent Abs
HTypeable Abs

data Abs_Attrs

Constructors

Abs_Attrs
Fields absVname :: String

Instances

Eq Abs_Attrs
Show Abs_Attrs
XmlAttributes Abs_Attrs

data TVar

Constructors

TVar TVar_Attrs [Class]

Instances

Eq TVar
Show TVar
XmlContent TVar
HTypeable TVar

data TVar_Attrs

Constructors

TVar_Attrs
Fields tVarName :: String tVarIndex :: Maybe String

Instances

Eq TVar_Attrs
Show TVar_Attrs
XmlAttributes TVar_Attrs

data TFree

Constructors

TFree TFree_Attrs [Class]

Instances

Eq TFree
Show TFree
XmlContent TFree
HTypeable TFree

data TFree_Attrs

Constructors

TFree_Attrs
Fields tFreeName :: String

Instances

Eq TFree_Attrs
Show TFree_Attrs
XmlAttributes TFree_Attrs

data Type

Constructors

Type Type_Attrs [OneOf3 TVar TFree Type]

Instances

Eq Type
Show Type
XmlContent Type
HTypeable Type

data Type_Attrs

Constructors

Type_Attrs
Fields typeName :: String

Instances

Eq Type_Attrs
Show Type_Attrs
XmlAttributes Type_Attrs

data Class

Constructors

Class
Fields className :: String

Instances

Eq Class
Show Class
XmlContent Class
XmlAttributes Class
HTypeable Class

Body_Locale Locale
Body_Cls Cls
Body_TypeSynonym TypeSynonym
Body_Datatypes Datatypes
Body_Domains Domains
Body_Consts Consts
Body_Axioms Axioms
Body_Lemma Lemma
Body_Definition Definition
Body_Funs Funs
Body_Primrec Primrec
Body_Fixrec Fixrec
Body_Instantiation Instantiation
Body_Instance Instance
Body_Subclass Subclass
Body_Typedef Typedef
Body_Defs Defs

Eq Body_
Show Body_
XmlContent Body_
HTypeable Body_