Safe Haskell	None

Isabelle.IsaExport

Documentation

newtype Export Source #

Constructors

Export (List1 Thy)

Instances

Instances details

Eq Export Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Export -> Export -> Bool (/=) :: Export -> Export -> Bool
Show Export Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Export -> ShowS show :: Export -> String showList :: [Export] -> ShowS
HTypeable Export Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Export -> HType
XmlContent Export Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Export toContents :: Export -> [Content ()] xToChar :: Export -> Char xFromChar :: Char -> Export

data Thy Source #

Constructors

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

Instances

Instances details

Eq Thy Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Thy -> Thy -> Bool (/=) :: Thy -> Thy -> Bool
Show Thy Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Thy -> ShowS show :: Thy -> String showList :: [Thy] -> ShowS
HTypeable Thy Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Thy -> HType
XmlContent Thy Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Thy toContents :: Thy -> [Content ()] xToChar :: Thy -> Char xFromChar :: Char -> Thy

data Thy_Attrs Source #

Constructors

Thy_Attrs
Fields thyName :: String thyHeader :: Maybe String

Instances

Instances details

Eq Thy_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Thy_Attrs -> Thy_Attrs -> Bool (/=) :: Thy_Attrs -> Thy_Attrs -> Bool
Show Thy_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Thy_Attrs -> ShowS show :: Thy_Attrs -> String showList :: [Thy_Attrs] -> ShowS
XmlAttributes Thy_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Thy_Attrs toAttrs :: Thy_Attrs -> [Attribute]

data Keyword Source #

Constructors

Keyword
Fields keywordName :: String

Instances

Instances details

Eq Keyword Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Keyword -> Keyword -> Bool (/=) :: Keyword -> Keyword -> Bool
Show Keyword Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Keyword -> ShowS show :: Keyword -> String showList :: [Keyword] -> ShowS
HTypeable Keyword Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Keyword -> HType
XmlAttributes Keyword Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Keyword toAttrs :: Keyword -> [Attribute]
XmlContent Keyword Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Keyword toContents :: Keyword -> [Content ()] xToChar :: Keyword -> Char xFromChar :: Char -> Keyword

data Import Source #

Constructors

Import
Fields importName :: String

Instances

Instances details

Eq Import Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Import -> Import -> Bool (/=) :: Import -> Import -> Bool
Show Import Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Import -> ShowS show :: Import -> String showList :: [Import] -> ShowS
HTypeable Import Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Import -> HType
XmlAttributes Import Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Import toAttrs :: Import -> [Attribute]
XmlContent Import Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Import toContents :: Import -> [Content ()] xToChar :: Import -> Char xFromChar :: Char -> Import

data UseFile Source #

Constructors

UseFile
Fields useFileName :: String

Instances

Instances details

Eq UseFile Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: UseFile -> UseFile -> Bool (/=) :: UseFile -> UseFile -> Bool
Show UseFile Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> UseFile -> ShowS show :: UseFile -> String showList :: [UseFile] -> ShowS
HTypeable UseFile Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: UseFile -> HType
XmlAttributes UseFile Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> UseFile toAttrs :: UseFile -> [Attribute]
XmlContent UseFile Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser UseFile toContents :: UseFile -> [Content ()] xToChar :: UseFile -> Char xFromChar :: Char -> UseFile

newtype Body Source #

Constructors

Body [Body_]

Instances

Instances details

Eq Body Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Body -> Body -> Bool (/=) :: Body -> Body -> Bool
Show Body Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Body -> ShowS show :: Body -> String showList :: [Body] -> ShowS
HTypeable Body Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Body -> HType
XmlContent Body Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Body toContents :: Body -> [Content ()] xToChar :: Body -> Char xFromChar :: Char -> Body

data Body_ Source #

Instances

Instances details

Eq Body_ Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Body_ -> Body_ -> Bool (/=) :: Body_ -> Body_ -> Bool
Show Body_ Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Body_ -> ShowS show :: Body_ -> String showList :: [Body_] -> ShowS
HTypeable Body_ Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Body_ -> HType
XmlContent Body_ Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Body_ toContents :: Body_ -> [Content ()] xToChar :: Body_ -> Char xFromChar :: Char -> Body_

data Locale Source #

Constructors

Locale Locale_Attrs Ctxt [Parent] Body

Instances

Instances details

Eq Locale Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Locale -> Locale -> Bool (/=) :: Locale -> Locale -> Bool
Show Locale Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Locale -> ShowS show :: Locale -> String showList :: [Locale] -> ShowS
HTypeable Locale Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Locale -> HType
XmlContent Locale Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Locale toContents :: Locale -> [Content ()] xToChar :: Locale -> Char xFromChar :: Char -> Locale

data Locale_Attrs Source #

Constructors

Locale_Attrs
Fields localeName :: String

Instances

Instances details

Eq Locale_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Locale_Attrs -> Locale_Attrs -> Bool (/=) :: Locale_Attrs -> Locale_Attrs -> Bool
Show Locale_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Locale_Attrs -> ShowS show :: Locale_Attrs -> String showList :: [Locale_Attrs] -> ShowS
XmlAttributes Locale_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Locale_Attrs toAttrs :: Locale_Attrs -> [Attribute]

data Cls Source #

Constructors

Cls Cls_Attrs Ctxt [Parent] Body

Instances

Instances details

Eq Cls Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Cls -> Cls -> Bool (/=) :: Cls -> Cls -> Bool
Show Cls Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Cls -> ShowS show :: Cls -> String showList :: [Cls] -> ShowS
HTypeable Cls Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Cls -> HType
XmlContent Cls Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Cls toContents :: Cls -> [Content ()] xToChar :: Cls -> Char xFromChar :: Char -> Cls

data Cls_Attrs Source #

Constructors

Cls_Attrs
Fields clsName :: String

Instances

Instances details

Eq Cls_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Cls_Attrs -> Cls_Attrs -> Bool (/=) :: Cls_Attrs -> Cls_Attrs -> Bool
Show Cls_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Cls_Attrs -> ShowS show :: Cls_Attrs -> String showList :: [Cls_Attrs] -> ShowS
XmlAttributes Cls_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Cls_Attrs toAttrs :: Cls_Attrs -> [Attribute]

data TypeSynonym Source #

Constructors

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

Instances

Instances details

Eq TypeSynonym Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: TypeSynonym -> TypeSynonym -> Bool (/=) :: TypeSynonym -> TypeSynonym -> Bool
Show TypeSynonym Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> TypeSynonym -> ShowS show :: TypeSynonym -> String showList :: [TypeSynonym] -> ShowS
HTypeable TypeSynonym Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: TypeSynonym -> HType
XmlContent TypeSynonym Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser TypeSynonym toContents :: TypeSynonym -> [Content ()] xToChar :: TypeSynonym -> Char xFromChar :: Char -> TypeSynonym

data TypeSynonym_Attrs Source #

Constructors

TypeSynonym_Attrs
Fields typeSynonymName :: String typeSynonymTarget :: Maybe String

Instances

Instances details

Eq TypeSynonym_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: TypeSynonym_Attrs -> TypeSynonym_Attrs -> Bool (/=) :: TypeSynonym_Attrs -> TypeSynonym_Attrs -> Bool
Show TypeSynonym_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> TypeSynonym_Attrs -> ShowS show :: TypeSynonym_Attrs -> String showList :: [TypeSynonym_Attrs] -> ShowS
XmlAttributes TypeSynonym_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> TypeSynonym_Attrs toAttrs :: TypeSynonym_Attrs -> [Attribute]

newtype Datatypes Source #

Constructors

Datatypes (List1 Datatype)

Instances

Instances details

Eq Datatypes Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Datatypes -> Datatypes -> Bool (/=) :: Datatypes -> Datatypes -> Bool
Show Datatypes Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Datatypes -> ShowS show :: Datatypes -> String showList :: [Datatypes] -> ShowS
HTypeable Datatypes Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Datatypes -> HType
XmlContent Datatypes Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Datatypes toContents :: Datatypes -> [Content ()] xToChar :: Datatypes -> Char xFromChar :: Char -> Datatypes

data Datatype Source #

Constructors

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

Instances

Instances details

Eq Datatype Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Datatype -> Datatype -> Bool (/=) :: Datatype -> Datatype -> Bool
Show Datatype Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Datatype -> ShowS show :: Datatype -> String showList :: [Datatype] -> ShowS
HTypeable Datatype Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Datatype -> HType
XmlContent Datatype Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Datatype toContents :: Datatype -> [Content ()] xToChar :: Datatype -> Char xFromChar :: Char -> Datatype

data Datatype_Attrs Source #

Constructors

Datatype_Attrs
Fields datatypeName :: String

Instances

Instances details

Eq Datatype_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Datatype_Attrs -> Datatype_Attrs -> Bool (/=) :: Datatype_Attrs -> Datatype_Attrs -> Bool
Show Datatype_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Datatype_Attrs -> ShowS show :: Datatype_Attrs -> String showList :: [Datatype_Attrs] -> ShowS
XmlAttributes Datatype_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Datatype_Attrs toAttrs :: Datatype_Attrs -> [Attribute]

data Constructor Source #

Constructors

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

Instances

Instances details

Eq Constructor Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Constructor -> Constructor -> Bool (/=) :: Constructor -> Constructor -> Bool
Show Constructor Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Constructor -> ShowS show :: Constructor -> String showList :: [Constructor] -> ShowS
HTypeable Constructor Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Constructor -> HType
XmlContent Constructor Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Constructor toContents :: Constructor -> [Content ()] xToChar :: Constructor -> Char xFromChar :: Char -> Constructor

data Constructor_Attrs Source #

Constructors

Constructor_Attrs
Fields constructorName :: Maybe String

Instances

Instances details

Eq Constructor_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Constructor_Attrs -> Constructor_Attrs -> Bool (/=) :: Constructor_Attrs -> Constructor_Attrs -> Bool
Show Constructor_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Constructor_Attrs -> ShowS show :: Constructor_Attrs -> String showList :: [Constructor_Attrs] -> ShowS
XmlAttributes Constructor_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Constructor_Attrs toAttrs :: Constructor_Attrs -> [Attribute]

newtype Domains Source #

Constructors

Domains (List1 Domain)

Instances

Instances details

Eq Domains Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Domains -> Domains -> Bool (/=) :: Domains -> Domains -> Bool
Show Domains Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Domains -> ShowS show :: Domains -> String showList :: [Domains] -> ShowS
HTypeable Domains Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Domains -> HType
XmlContent Domains Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Domains toContents :: Domains -> [Content ()] xToChar :: Domains -> Char xFromChar :: Char -> Domains

data Domain Source #

Constructors

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

Instances

Instances details

Eq Domain Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Domain -> Domain -> Bool (/=) :: Domain -> Domain -> Bool
Show Domain Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Domain -> ShowS show :: Domain -> String showList :: [Domain] -> ShowS
HTypeable Domain Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Domain -> HType
XmlContent Domain Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Domain toContents :: Domain -> [Content ()] xToChar :: Domain -> Char xFromChar :: Char -> Domain

data Domain_Attrs Source #

Constructors

Domain_Attrs
Fields domainName :: String

Instances

Instances details

Eq Domain_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Domain_Attrs -> Domain_Attrs -> Bool (/=) :: Domain_Attrs -> Domain_Attrs -> Bool
Show Domain_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Domain_Attrs -> ShowS show :: Domain_Attrs -> String showList :: [Domain_Attrs] -> ShowS
XmlAttributes Domain_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Domain_Attrs toAttrs :: Domain_Attrs -> [Attribute]

data DomainConstructor Source #

Constructors

DomainConstructor DomainConstructor_Attrs (OneOf3 TVar TFree Type) [DomainConstructorArg]

Instances

Instances details

Eq DomainConstructor Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: DomainConstructor -> DomainConstructor -> Bool (/=) :: DomainConstructor -> DomainConstructor -> Bool
Show DomainConstructor Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> DomainConstructor -> ShowS show :: DomainConstructor -> String showList :: [DomainConstructor] -> ShowS
HTypeable DomainConstructor Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: DomainConstructor -> HType
XmlContent DomainConstructor Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser DomainConstructor toContents :: DomainConstructor -> [Content ()] xToChar :: DomainConstructor -> Char xFromChar :: Char -> DomainConstructor

data DomainConstructor_Attrs Source #

Constructors

DomainConstructor_Attrs
Fields domainConstructorName :: String

Instances

Instances details

Eq DomainConstructor_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: DomainConstructor_Attrs -> DomainConstructor_Attrs -> Bool (/=) :: DomainConstructor_Attrs -> DomainConstructor_Attrs -> Bool
Show DomainConstructor_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> DomainConstructor_Attrs -> ShowS show :: DomainConstructor_Attrs -> String showList :: [DomainConstructor_Attrs] -> ShowS
XmlAttributes DomainConstructor_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> DomainConstructor_Attrs toAttrs :: DomainConstructor_Attrs -> [Attribute]

data DomainConstructorArg Source #

Constructors

DomainConstructorArg DomainConstructorArg_Attrs (OneOf3 TVar TFree Type)

Instances

Instances details

Eq DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: DomainConstructorArg -> DomainConstructorArg -> Bool (/=) :: DomainConstructorArg -> DomainConstructorArg -> Bool
Show DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> DomainConstructorArg -> ShowS show :: DomainConstructorArg -> String showList :: [DomainConstructorArg] -> ShowS
HTypeable DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: DomainConstructorArg -> HType
XmlContent DomainConstructorArg Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser DomainConstructorArg toContents :: DomainConstructorArg -> [Content ()] xToChar :: DomainConstructorArg -> Char xFromChar :: Char -> DomainConstructorArg

data DomainConstructorArg_Attrs Source #

Constructors

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

Instances

Instances details

Eq DomainConstructorArg_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: DomainConstructorArg_Attrs -> DomainConstructorArg_Attrs -> Bool (/=) :: DomainConstructorArg_Attrs -> DomainConstructorArg_Attrs -> Bool
Show DomainConstructorArg_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> DomainConstructorArg_Attrs -> ShowS show :: DomainConstructorArg_Attrs -> String showList :: [DomainConstructorArg_Attrs] -> ShowS
XmlAttributes DomainConstructorArg_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> DomainConstructorArg_Attrs toAttrs :: DomainConstructorArg_Attrs -> [Attribute]

newtype Consts Source #

Constructors

Consts (List1 ConstDef)

Instances

Instances details

Eq Consts Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Consts -> Consts -> Bool (/=) :: Consts -> Consts -> Bool
Show Consts Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Consts -> ShowS show :: Consts -> String showList :: [Consts] -> ShowS
HTypeable Consts Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Consts -> HType
XmlContent Consts Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Consts toContents :: Consts -> [Content ()] xToChar :: Consts -> Char xFromChar :: Char -> Consts

data ConstDef Source #

Constructors

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

Instances

Instances details

Eq ConstDef Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: ConstDef -> ConstDef -> Bool (/=) :: ConstDef -> ConstDef -> Bool
Show ConstDef Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> ConstDef -> ShowS show :: ConstDef -> String showList :: [ConstDef] -> ShowS
HTypeable ConstDef Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: ConstDef -> HType
XmlContent ConstDef Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser ConstDef toContents :: ConstDef -> [Content ()] xToChar :: ConstDef -> Char xFromChar :: Char -> ConstDef

data ConstDef_Attrs Source #

Constructors

ConstDef_Attrs
Fields constDefName :: String

Instances

Instances details

Eq ConstDef_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: ConstDef_Attrs -> ConstDef_Attrs -> Bool (/=) :: ConstDef_Attrs -> ConstDef_Attrs -> Bool
Show ConstDef_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> ConstDef_Attrs -> ShowS show :: ConstDef_Attrs -> String showList :: [ConstDef_Attrs] -> ShowS
XmlAttributes ConstDef_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> ConstDef_Attrs toAttrs :: ConstDef_Attrs -> [Attribute]

newtype Axioms Source #

Constructors

Axioms (List1 Axiom)

Instances

Instances details

Eq Axioms Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Axioms -> Axioms -> Bool (/=) :: Axioms -> Axioms -> Bool
Show Axioms Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Axioms -> ShowS show :: Axioms -> String showList :: [Axioms] -> ShowS
HTypeable Axioms Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Axioms -> HType
XmlContent Axioms Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Axioms toContents :: Axioms -> [Content ()] xToChar :: Axioms -> Char xFromChar :: Char -> Axioms

data Axiom Source #

Constructors

Axiom Axiom_Attrs (OneOf6 Bound Free Var Const App Abs)

Instances

Instances details

Eq Axiom Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Axiom -> Axiom -> Bool (/=) :: Axiom -> Axiom -> Bool
Show Axiom Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Axiom -> ShowS show :: Axiom -> String showList :: [Axiom] -> ShowS
HTypeable Axiom Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Axiom -> HType
XmlContent Axiom Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Axiom toContents :: Axiom -> [Content ()] xToChar :: Axiom -> Char xFromChar :: Char -> Axiom

data Axiom_Attrs Source #

Constructors

Axiom_Attrs
Fields axiomName :: String axiomArgs :: String

Instances

Instances details

Eq Axiom_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Axiom_Attrs -> Axiom_Attrs -> Bool (/=) :: Axiom_Attrs -> Axiom_Attrs -> Bool
Show Axiom_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Axiom_Attrs -> ShowS show :: Axiom_Attrs -> String showList :: [Axiom_Attrs] -> ShowS
XmlAttributes Axiom_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Axiom_Attrs toAttrs :: Axiom_Attrs -> [Attribute]

data Lemma Source #

Constructors

Lemma Lemma_Attrs Ctxt Proof (List1 Shows)

Instances

Instances details

Eq Lemma Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Lemma -> Lemma -> Bool (/=) :: Lemma -> Lemma -> Bool
Show Lemma Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Lemma -> ShowS show :: Lemma -> String showList :: [Lemma] -> ShowS
HTypeable Lemma Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Lemma -> HType
XmlContent Lemma Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Lemma toContents :: Lemma -> [Content ()] xToChar :: Lemma -> Char xFromChar :: Char -> Lemma

data Lemma_Attrs Source #

Constructors

Lemma_Attrs
Fields lemmaTarget :: Maybe String

Instances

Instances details

Eq Lemma_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Lemma_Attrs -> Lemma_Attrs -> Bool (/=) :: Lemma_Attrs -> Lemma_Attrs -> Bool
Show Lemma_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Lemma_Attrs -> ShowS show :: Lemma_Attrs -> String showList :: [Lemma_Attrs] -> ShowS
XmlAttributes Lemma_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Lemma_Attrs toAttrs :: Lemma_Attrs -> [Attribute]

data Definition Source #

Constructors

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

Instances

Instances details

Eq Definition Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Definition -> Definition -> Bool (/=) :: Definition -> Definition -> Bool
Show Definition Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Definition -> ShowS show :: Definition -> String showList :: [Definition] -> ShowS
HTypeable Definition Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Definition -> HType
XmlContent Definition Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Definition toContents :: Definition -> [Content ()] xToChar :: Definition -> Char xFromChar :: Char -> Definition

data Definition_Attrs Source #

Constructors

Definition_Attrs
Fields definitionName :: String definitionTarget :: Maybe String

Instances

Instances details

Eq Definition_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Definition_Attrs -> Definition_Attrs -> Bool (/=) :: Definition_Attrs -> Definition_Attrs -> Bool
Show Definition_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Definition_Attrs -> ShowS show :: Definition_Attrs -> String showList :: [Definition_Attrs] -> ShowS
XmlAttributes Definition_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Definition_Attrs toAttrs :: Definition_Attrs -> [Attribute]

data Funs Source #

Constructors

Funs Funs_Attrs (List1 Fun)

Instances

Instances details

Eq Funs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Funs -> Funs -> Bool (/=) :: Funs -> Funs -> Bool
Show Funs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Funs -> ShowS show :: Funs -> String showList :: [Funs] -> ShowS
HTypeable Funs Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Funs -> HType
XmlContent Funs Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Funs toContents :: Funs -> [Content ()] xToChar :: Funs -> Char xFromChar :: Char -> Funs

data Funs_Attrs Source #

Constructors

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

Instances

Instances details

Eq Funs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Funs_Attrs -> Funs_Attrs -> Bool (/=) :: Funs_Attrs -> Funs_Attrs -> Bool
Show Funs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Funs_Attrs -> ShowS show :: Funs_Attrs -> String showList :: [Funs_Attrs] -> ShowS
XmlAttributes Funs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Funs_Attrs toAttrs :: Funs_Attrs -> [Attribute]

data Fun Source #

Constructors

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

Instances

Instances details

Eq Fun Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Fun -> Fun -> Bool (/=) :: Fun -> Fun -> Bool
Show Fun Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Fun -> ShowS show :: Fun -> String showList :: [Fun] -> ShowS
HTypeable Fun Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Fun -> HType
XmlContent Fun Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Fun toContents :: Fun -> [Content ()] xToChar :: Fun -> Char xFromChar :: Char -> Fun

data Fun_Attrs Source #

Constructors

Fun_Attrs
Fields funName :: String

Instances

Instances details

Eq Fun_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Fun_Attrs -> Fun_Attrs -> Bool (/=) :: Fun_Attrs -> Fun_Attrs -> Bool
Show Fun_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Fun_Attrs -> ShowS show :: Fun_Attrs -> String showList :: [Fun_Attrs] -> ShowS
XmlAttributes Fun_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Fun_Attrs toAttrs :: Fun_Attrs -> [Attribute]

newtype Equation Source #

Constructors

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

Instances

Instances details

Eq Equation Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Equation -> Equation -> Bool (/=) :: Equation -> Equation -> Bool
Show Equation Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Equation -> ShowS show :: Equation -> String showList :: [Equation] -> ShowS
HTypeable Equation Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Equation -> HType
XmlContent Equation Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Equation toContents :: Equation -> [Content ()] xToChar :: Equation -> Char xFromChar :: Char -> Equation

data Primrec Source #

Constructors

Primrec Primrec_Attrs (List1 Fun)

Instances

Instances details

Eq Primrec Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Primrec -> Primrec -> Bool (/=) :: Primrec -> Primrec -> Bool
Show Primrec Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Primrec -> ShowS show :: Primrec -> String showList :: [Primrec] -> ShowS
HTypeable Primrec Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Primrec -> HType
XmlContent Primrec Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Primrec toContents :: Primrec -> [Content ()] xToChar :: Primrec -> Char xFromChar :: Char -> Primrec

data Primrec_Attrs Source #

Constructors

Primrec_Attrs
Fields primrecTarget :: Maybe String

Instances

Instances details

Eq Primrec_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Primrec_Attrs -> Primrec_Attrs -> Bool (/=) :: Primrec_Attrs -> Primrec_Attrs -> Bool
Show Primrec_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Primrec_Attrs -> ShowS show :: Primrec_Attrs -> String showList :: [Primrec_Attrs] -> ShowS
XmlAttributes Primrec_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Primrec_Attrs toAttrs :: Primrec_Attrs -> [Attribute]

newtype Fixrec Source #

Constructors

Fixrec (List1 FixrecFun)

Instances

Instances details

Eq Fixrec Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Fixrec -> Fixrec -> Bool (/=) :: Fixrec -> Fixrec -> Bool
Show Fixrec Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Fixrec -> ShowS show :: Fixrec -> String showList :: [Fixrec] -> ShowS
HTypeable Fixrec Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Fixrec -> HType
XmlContent Fixrec Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Fixrec toContents :: Fixrec -> [Content ()] xToChar :: Fixrec -> Char xFromChar :: Char -> Fixrec

data FixrecFun Source #

Constructors

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

Instances

Instances details

Eq FixrecFun Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: FixrecFun -> FixrecFun -> Bool (/=) :: FixrecFun -> FixrecFun -> Bool
Show FixrecFun Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> FixrecFun -> ShowS show :: FixrecFun -> String showList :: [FixrecFun] -> ShowS
HTypeable FixrecFun Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: FixrecFun -> HType
XmlContent FixrecFun Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser FixrecFun toContents :: FixrecFun -> [Content ()] xToChar :: FixrecFun -> Char xFromChar :: Char -> FixrecFun

data FixrecFun_Attrs Source #

Constructors

FixrecFun_Attrs
Fields fixrecFunName :: String

Instances

Instances details

Eq FixrecFun_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: FixrecFun_Attrs -> FixrecFun_Attrs -> Bool (/=) :: FixrecFun_Attrs -> FixrecFun_Attrs -> Bool
Show FixrecFun_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> FixrecFun_Attrs -> ShowS show :: FixrecFun_Attrs -> String showList :: [FixrecFun_Attrs] -> ShowS
XmlAttributes FixrecFun_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> FixrecFun_Attrs toAttrs :: FixrecFun_Attrs -> [Attribute]

data FixrecEquation Source #

Constructors

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

Instances

Instances details

Eq FixrecEquation Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: FixrecEquation -> FixrecEquation -> Bool (/=) :: FixrecEquation -> FixrecEquation -> Bool
Show FixrecEquation Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> FixrecEquation -> ShowS show :: FixrecEquation -> String showList :: [FixrecEquation] -> ShowS
HTypeable FixrecEquation Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: FixrecEquation -> HType
XmlContent FixrecEquation Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser FixrecEquation toContents :: FixrecEquation -> [Content ()] xToChar :: FixrecEquation -> Char xFromChar :: Char -> FixrecEquation

data FixrecEquation_Attrs Source #

Constructors

FixrecEquation_Attrs
Fields fixrecEquationUnchecked :: Maybe String

Instances

Instances details

Eq FixrecEquation_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: FixrecEquation_Attrs -> FixrecEquation_Attrs -> Bool (/=) :: FixrecEquation_Attrs -> FixrecEquation_Attrs -> Bool
Show FixrecEquation_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> FixrecEquation_Attrs -> ShowS show :: FixrecEquation_Attrs -> String showList :: [FixrecEquation_Attrs] -> ShowS
XmlAttributes FixrecEquation_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> FixrecEquation_Attrs toAttrs :: FixrecEquation_Attrs -> [Attribute]

newtype Premises Source #

Constructors

Premises [OneOf6 Bound Free Var Const App Abs]

Instances

Instances details

Eq Premises Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Premises -> Premises -> Bool (/=) :: Premises -> Premises -> Bool
Show Premises Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Premises -> ShowS show :: Premises -> String showList :: [Premises] -> ShowS
HTypeable Premises Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Premises -> HType
XmlContent Premises Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Premises toContents :: Premises -> [Content ()] xToChar :: Premises -> Char xFromChar :: Char -> Premises

data Instantiation Source #

Constructors

Instantiation Instantiation_Attrs Arity Body

Instances

Instances details

Eq Instantiation Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Instantiation -> Instantiation -> Bool (/=) :: Instantiation -> Instantiation -> Bool
Show Instantiation Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Instantiation -> ShowS show :: Instantiation -> String showList :: [Instantiation] -> ShowS
HTypeable Instantiation Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Instantiation -> HType
XmlContent Instantiation Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Instantiation toContents :: Instantiation -> [Content ()] xToChar :: Instantiation -> Char xFromChar :: Char -> Instantiation

data Instantiation_Attrs Source #

Constructors

Instantiation_Attrs
Fields instantiationType :: String

Instances

Instances details

Eq Instantiation_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Instantiation_Attrs -> Instantiation_Attrs -> Bool (/=) :: Instantiation_Attrs -> Instantiation_Attrs -> Bool
Show Instantiation_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Instantiation_Attrs -> ShowS show :: Instantiation_Attrs -> String showList :: [Instantiation_Attrs] -> ShowS
XmlAttributes Instantiation_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Instantiation_Attrs toAttrs :: Instantiation_Attrs -> [Attribute]

data Instance Source #

Constructors

Instance Instance_Attrs Proof (Maybe (Vars, Arity))

Instances

Instances details

Eq Instance Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Instance -> Instance -> Bool (/=) :: Instance -> Instance -> Bool
Show Instance Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Instance -> ShowS show :: Instance -> String showList :: [Instance] -> ShowS
HTypeable Instance Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Instance -> HType
XmlContent Instance Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Instance toContents :: Instance -> [Content ()] xToChar :: Instance -> Char xFromChar :: Char -> Instance

data Instance_Attrs Source #

Constructors

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

Instances

Instances details

Eq Instance_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Instance_Attrs -> Instance_Attrs -> Bool (/=) :: Instance_Attrs -> Instance_Attrs -> Bool
Show Instance_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Instance_Attrs -> ShowS show :: Instance_Attrs -> String showList :: [Instance_Attrs] -> ShowS
XmlAttributes Instance_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Instance_Attrs toAttrs :: Instance_Attrs -> [Attribute]

data Subclass Source #

Constructors

Subclass Subclass_Attrs Proof

Instances

Instances details

Eq Subclass Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Subclass -> Subclass -> Bool (/=) :: Subclass -> Subclass -> Bool
Show Subclass Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Subclass -> ShowS show :: Subclass -> String showList :: [Subclass] -> ShowS
HTypeable Subclass Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Subclass -> HType
XmlContent Subclass Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Subclass toContents :: Subclass -> [Content ()] xToChar :: Subclass -> Char xFromChar :: Char -> Subclass

data Subclass_Attrs Source #

Constructors

Subclass_Attrs
Fields subclassClass :: String subclassTarget :: Maybe String

Instances

Instances details

Eq Subclass_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Subclass_Attrs -> Subclass_Attrs -> Bool (/=) :: Subclass_Attrs -> Subclass_Attrs -> Bool
Show Subclass_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Subclass_Attrs -> ShowS show :: Subclass_Attrs -> String showList :: [Subclass_Attrs] -> ShowS
XmlAttributes Subclass_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Subclass_Attrs toAttrs :: Subclass_Attrs -> [Attribute]

data Typedef Source #

Constructors

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

Instances

Instances details

Eq Typedef Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Typedef -> Typedef -> Bool (/=) :: Typedef -> Typedef -> Bool
Show Typedef Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Typedef -> ShowS show :: Typedef -> String showList :: [Typedef] -> ShowS
HTypeable Typedef Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Typedef -> HType
XmlContent Typedef Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Typedef toContents :: Typedef -> [Content ()] xToChar :: Typedef -> Char xFromChar :: Char -> Typedef

data Typedef_Attrs Source #

Constructors

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

Instances

Instances details

Eq Typedef_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Typedef_Attrs -> Typedef_Attrs -> Bool (/=) :: Typedef_Attrs -> Typedef_Attrs -> Bool
Show Typedef_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Typedef_Attrs -> ShowS show :: Typedef_Attrs -> String showList :: [Typedef_Attrs] -> ShowS
XmlAttributes Typedef_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Typedef_Attrs toAttrs :: Typedef_Attrs -> [Attribute]

data Defs Source #

Constructors

Defs Defs_Attrs (List1 Def)

Instances

Instances details

Eq Defs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Defs -> Defs -> Bool (/=) :: Defs -> Defs -> Bool
Show Defs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Defs -> ShowS show :: Defs -> String showList :: [Defs] -> ShowS
HTypeable Defs Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Defs -> HType
XmlContent Defs Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Defs toContents :: Defs -> [Content ()] xToChar :: Defs -> Char xFromChar :: Char -> Defs

data Defs_Attrs Source #

Constructors

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

Instances

Instances details

Eq Defs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Defs_Attrs -> Defs_Attrs -> Bool (/=) :: Defs_Attrs -> Defs_Attrs -> Bool
Show Defs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Defs_Attrs -> ShowS show :: Defs_Attrs -> String showList :: [Defs_Attrs] -> ShowS
XmlAttributes Defs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Defs_Attrs toAttrs :: Defs_Attrs -> [Attribute]

data Def Source #

Constructors

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

Instances

Instances details

Eq Def Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Def -> Def -> Bool (/=) :: Def -> Def -> Bool
Show Def Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Def -> ShowS show :: Def -> String showList :: [Def] -> ShowS
HTypeable Def Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Def -> HType
XmlContent Def Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Def toContents :: Def -> [Content ()] xToChar :: Def -> Char xFromChar :: Char -> Def

data Def_Attrs Source #

Constructors

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

Instances

Instances details

Eq Def_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Def_Attrs -> Def_Attrs -> Bool (/=) :: Def_Attrs -> Def_Attrs -> Bool
Show Def_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Def_Attrs -> ShowS show :: Def_Attrs -> String showList :: [Def_Attrs] -> ShowS
XmlAttributes Def_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Def_Attrs toAttrs :: Def_Attrs -> [Attribute]

newtype Sort Source #

Constructors

Sort (List1 Class)

Instances

Instances details

Eq Sort Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Sort -> Sort -> Bool (/=) :: Sort -> Sort -> Bool
Show Sort Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Sort -> ShowS show :: Sort -> String showList :: [Sort] -> ShowS
HTypeable Sort Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Sort -> HType
XmlContent Sort Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Sort toContents :: Sort -> [Content ()] xToChar :: Sort -> Char xFromChar :: Char -> Sort

data Arity Source #

Constructors

Arity Sort [Sort]

Instances

Instances details

Eq Arity Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Arity -> Arity -> Bool (/=) :: Arity -> Arity -> Bool
Show Arity Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Arity -> ShowS show :: Arity -> String showList :: [Arity] -> ShowS
HTypeable Arity Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Arity -> HType
XmlContent Arity Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Arity toContents :: Arity -> [Content ()] xToChar :: Arity -> Char xFromChar :: Char -> Arity

newtype Vars Source #

Constructors

Vars [TFree]

Instances

Instances details

Eq Vars Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Vars -> Vars -> Bool (/=) :: Vars -> Vars -> Bool
Show Vars Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Vars -> ShowS show :: Vars -> String showList :: [Vars] -> ShowS
HTypeable Vars Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Vars -> HType
XmlContent Vars Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Vars toContents :: Vars -> [Content ()] xToChar :: Vars -> Char xFromChar :: Char -> Vars

data Parent Source #

Constructors

Parent
Fields parentName :: String

Instances

Instances details

Eq Parent Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Parent -> Parent -> Bool (/=) :: Parent -> Parent -> Bool
Show Parent Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Parent -> ShowS show :: Parent -> String showList :: [Parent] -> ShowS
HTypeable Parent Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Parent -> HType
XmlAttributes Parent Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Parent toAttrs :: Parent -> [Attribute]
XmlContent Parent Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Parent toContents :: Parent -> [Content ()] xToChar :: Parent -> Char xFromChar :: Char -> Parent

newtype Fixes Source #

Constructors

Fixes [Fix]

Instances

Instances details

Eq Fixes Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Fixes -> Fixes -> Bool (/=) :: Fixes -> Fixes -> Bool
Show Fixes Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Fixes -> ShowS show :: Fixes -> String showList :: [Fixes] -> ShowS
HTypeable Fixes Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Fixes -> HType
XmlContent Fixes Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Fixes toContents :: Fixes -> [Content ()] xToChar :: Fixes -> Char xFromChar :: Char -> Fixes

data Fix Source #

Constructors

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

Instances

Instances details

Eq Fix Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Fix -> Fix -> Bool (/=) :: Fix -> Fix -> Bool
Show Fix Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Fix -> ShowS show :: Fix -> String showList :: [Fix] -> ShowS
HTypeable Fix Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Fix -> HType
XmlContent Fix Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Fix toContents :: Fix -> [Content ()] xToChar :: Fix -> Char xFromChar :: Char -> Fix

data Fix_Attrs Source #

Constructors

Fix_Attrs
Fields fixName :: String

Instances

Instances details

Eq Fix_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Fix_Attrs -> Fix_Attrs -> Bool (/=) :: Fix_Attrs -> Fix_Attrs -> Bool
Show Fix_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Fix_Attrs -> ShowS show :: Fix_Attrs -> String showList :: [Fix_Attrs] -> ShowS
XmlAttributes Fix_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Fix_Attrs toAttrs :: Fix_Attrs -> [Attribute]

newtype Assumes Source #

Constructors

Assumes [Assumption]

Instances

Instances details

Eq Assumes Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Assumes -> Assumes -> Bool (/=) :: Assumes -> Assumes -> Bool
Show Assumes Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Assumes -> ShowS show :: Assumes -> String showList :: [Assumes] -> ShowS
HTypeable Assumes Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Assumes -> HType
XmlContent Assumes Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Assumes toContents :: Assumes -> [Content ()] xToChar :: Assumes -> Char xFromChar :: Char -> Assumes

data Assumption Source #

Constructors

Assumption Assumption_Attrs (OneOf6 Bound Free Var Const App Abs)

Instances

Instances details

Eq Assumption Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Assumption -> Assumption -> Bool (/=) :: Assumption -> Assumption -> Bool
Show Assumption Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Assumption -> ShowS show :: Assumption -> String showList :: [Assumption] -> ShowS
HTypeable Assumption Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Assumption -> HType
XmlContent Assumption Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Assumption toContents :: Assumption -> [Content ()] xToChar :: Assumption -> Char xFromChar :: Char -> Assumption

data Assumption_Attrs Source #

Constructors

Assumption_Attrs
Fields assumptionName :: String assumptionArgs :: String

Instances

Instances details

Eq Assumption_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Assumption_Attrs -> Assumption_Attrs -> Bool (/=) :: Assumption_Attrs -> Assumption_Attrs -> Bool
Show Assumption_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Assumption_Attrs -> ShowS show :: Assumption_Attrs -> String showList :: [Assumption_Attrs] -> ShowS
XmlAttributes Assumption_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Assumption_Attrs toAttrs :: Assumption_Attrs -> [Attribute]

newtype Ctxt Source #

Constructors

Ctxt [OneOf2 Fixes Assumes]

Instances

Instances details

Eq Ctxt Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Ctxt -> Ctxt -> Bool (/=) :: Ctxt -> Ctxt -> Bool
Show Ctxt Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Ctxt -> ShowS show :: Ctxt -> String showList :: [Ctxt] -> ShowS
HTypeable Ctxt Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Ctxt -> HType
XmlContent Ctxt Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Ctxt toContents :: Ctxt -> [Content ()] xToChar :: Ctxt -> Char xFromChar :: Char -> Ctxt

data Mixfix Source #

Constructors

Mixfix Mixfix_Attrs [OneOf4 Arg AString Break Block]

Instances

Instances details

Eq Mixfix Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Mixfix -> Mixfix -> Bool (/=) :: Mixfix -> Mixfix -> Bool
Show Mixfix Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Mixfix -> ShowS show :: Mixfix -> String showList :: [Mixfix] -> ShowS
HTypeable Mixfix Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Mixfix -> HType
XmlContent Mixfix Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Mixfix toContents :: Mixfix -> [Content ()] xToChar :: Mixfix -> Char xFromChar :: Char -> Mixfix

data Mixfix_Attrs Source #

Constructors

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

Instances

Instances details

Eq Mixfix_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Mixfix_Attrs -> Mixfix_Attrs -> Bool (/=) :: Mixfix_Attrs -> Mixfix_Attrs -> Bool
Show Mixfix_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Mixfix_Attrs -> ShowS show :: Mixfix_Attrs -> String showList :: [Mixfix_Attrs] -> ShowS
XmlAttributes Mixfix_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Mixfix_Attrs toAttrs :: Mixfix_Attrs -> [Attribute]

data Arg Source #

Constructors

Arg
Fields argPrio :: String

Instances

Instances details

Eq Arg Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Arg -> Arg -> Bool (/=) :: Arg -> Arg -> Bool
Show Arg Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Arg -> ShowS show :: Arg -> String showList :: [Arg] -> ShowS
HTypeable Arg Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Arg -> HType
XmlAttributes Arg Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Arg toAttrs :: Arg -> [Attribute]
XmlContent Arg Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Arg toContents :: Arg -> [Content ()] xToChar :: Arg -> Char xFromChar :: Char -> Arg

data AString Source #

Constructors

AString
Fields stringVal :: String

Instances

Instances details

Eq AString Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: AString -> AString -> Bool (/=) :: AString -> AString -> Bool
Show AString Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> AString -> ShowS show :: AString -> String showList :: [AString] -> ShowS
HTypeable AString Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: AString -> HType
XmlAttributes AString Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> AString toAttrs :: AString -> [Attribute]
XmlContent AString Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser AString toContents :: AString -> [Content ()] xToChar :: AString -> Char xFromChar :: Char -> AString

data Break Source #

Constructors

Break
Fields breakPrio :: String

Instances

Instances details

Eq Break Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Break -> Break -> Bool (/=) :: Break -> Break -> Bool
Show Break Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Break -> ShowS show :: Break -> String showList :: [Break] -> ShowS
HTypeable Break Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Break -> HType
XmlAttributes Break Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Break toAttrs :: Break -> [Attribute]
XmlContent Break Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Break toContents :: Break -> [Content ()] xToChar :: Break -> Char xFromChar :: Char -> Break

data Block Source #

Constructors

Block Block_Attrs [OneOf4 Arg AString Break Block]

Instances

Instances details

Eq Block Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Block -> Block -> Bool (/=) :: Block -> Block -> Bool
Show Block Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Block -> ShowS show :: Block -> String showList :: [Block] -> ShowS
HTypeable Block Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Block -> HType
XmlContent Block Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Block toContents :: Block -> [Content ()] xToChar :: Block -> Char xFromChar :: Char -> Block

data Block_Attrs Source #

Constructors

Block_Attrs
Fields blockPrio :: String

Instances

Instances details

Eq Block_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Block_Attrs -> Block_Attrs -> Bool (/=) :: Block_Attrs -> Block_Attrs -> Bool
Show Block_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Block_Attrs -> ShowS show :: Block_Attrs -> String showList :: [Block_Attrs] -> ShowS
XmlAttributes Block_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Block_Attrs toAttrs :: Block_Attrs -> [Attribute]

newtype Proof Source #

Constructors

Proof String

Instances

Instances details

Eq Proof Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Proof -> Proof -> Bool (/=) :: Proof -> Proof -> Bool
Show Proof Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Proof -> ShowS show :: Proof -> String showList :: [Proof] -> ShowS
HTypeable Proof Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Proof -> HType
XmlContent Proof Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Proof toContents :: Proof -> [Content ()] xToChar :: Proof -> Char xFromChar :: Char -> Proof

data Shows Source #

Constructors

Shows Shows_Attrs (List1 AShow)

Instances

Instances details

Eq Shows Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Shows -> Shows -> Bool (/=) :: Shows -> Shows -> Bool
Show Shows Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Shows -> ShowS show :: Shows -> String showList :: [Shows] -> ShowS
HTypeable Shows Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Shows -> HType
XmlContent Shows Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Shows toContents :: Shows -> [Content ()] xToChar :: Shows -> Char xFromChar :: Char -> Shows

data Shows_Attrs Source #

Constructors

Shows_Attrs
Fields showsName :: String showsArgs :: Maybe String

Instances

Instances details

Eq Shows_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Shows_Attrs -> Shows_Attrs -> Bool (/=) :: Shows_Attrs -> Shows_Attrs -> Bool
Show Shows_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Shows_Attrs -> ShowS show :: Shows_Attrs -> String showList :: [Shows_Attrs] -> ShowS
XmlAttributes Shows_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Shows_Attrs toAttrs :: Shows_Attrs -> [Attribute]

newtype AShow Source #

Constructors

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

Instances

Instances details

Eq AShow Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: AShow -> AShow -> Bool (/=) :: AShow -> AShow -> Bool
Show AShow Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> AShow -> ShowS show :: AShow -> String showList :: [AShow] -> ShowS
HTypeable AShow Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: AShow -> HType
XmlContent AShow Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser AShow toContents :: AShow -> [Content ()] xToChar :: AShow -> Char xFromChar :: Char -> AShow

data Bound Source #

Constructors

Bound
Fields boundIndex :: String

Instances

Instances details

Eq Bound Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Bound -> Bound -> Bool (/=) :: Bound -> Bound -> Bool
Show Bound Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Bound -> ShowS show :: Bound -> String showList :: [Bound] -> ShowS
HTypeable Bound Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Bound -> HType
XmlAttributes Bound Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Bound toAttrs :: Bound -> [Attribute]
XmlContent Bound Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Bound toContents :: Bound -> [Content ()] xToChar :: Bound -> Char xFromChar :: Char -> Bound

data Free Source #

Constructors

FreeTVar Free_Attrs TVar
FreeTFree Free_Attrs TFree
FreeType Free_Attrs Type

Instances

Instances details

Eq Free Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Free -> Free -> Bool (/=) :: Free -> Free -> Bool
Show Free Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Free -> ShowS show :: Free -> String showList :: [Free] -> ShowS
HTypeable Free Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Free -> HType
XmlContent Free Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Free toContents :: Free -> [Content ()] xToChar :: Free -> Char xFromChar :: Char -> Free

data Free_Attrs Source #

Constructors

Free_Attrs
Fields freeName :: String

Instances

Instances details

Eq Free_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Free_Attrs -> Free_Attrs -> Bool (/=) :: Free_Attrs -> Free_Attrs -> Bool
Show Free_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Free_Attrs -> ShowS show :: Free_Attrs -> String showList :: [Free_Attrs] -> ShowS
XmlAttributes Free_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Free_Attrs toAttrs :: Free_Attrs -> [Attribute]

data Var Source #

Constructors

VarTVar Var_Attrs TVar
VarTFree Var_Attrs TFree
VarType Var_Attrs Type

Instances

Instances details

Eq Var Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Var -> Var -> Bool (/=) :: Var -> Var -> Bool
Show Var Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Var -> ShowS show :: Var -> String showList :: [Var] -> ShowS
HTypeable Var Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Var -> HType
XmlContent Var Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Var toContents :: Var -> [Content ()] xToChar :: Var -> Char xFromChar :: Char -> Var

data Var_Attrs Source #

Constructors

Var_Attrs
Fields varName :: String varIndex :: Maybe String

Instances

Instances details

Eq Var_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Var_Attrs -> Var_Attrs -> Bool (/=) :: Var_Attrs -> Var_Attrs -> Bool
Show Var_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Var_Attrs -> ShowS show :: Var_Attrs -> String showList :: [Var_Attrs] -> ShowS
XmlAttributes Var_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Var_Attrs toAttrs :: Var_Attrs -> [Attribute]

data Const Source #

Constructors

Const Const_Attrs (OneOf3 TVar TFree Type)

Instances

Instances details

Eq Const Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Const -> Const -> Bool (/=) :: Const -> Const -> Bool
Show Const Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Const -> ShowS show :: Const -> String showList :: [Const] -> ShowS
HTypeable Const Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Const -> HType
XmlContent Const Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Const toContents :: Const -> [Content ()] xToChar :: Const -> Char xFromChar :: Char -> Const

data Const_Attrs Source #

Constructors

Const_Attrs
Fields constName :: String

Instances

Instances details

Eq Const_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Const_Attrs -> Const_Attrs -> Bool (/=) :: Const_Attrs -> Const_Attrs -> Bool
Show Const_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Const_Attrs -> ShowS show :: Const_Attrs -> String showList :: [Const_Attrs] -> ShowS
XmlAttributes Const_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Const_Attrs toAttrs :: Const_Attrs -> [Attribute]

data App Source #

Constructors

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

Instances

Instances details

Eq App Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: App -> App -> Bool (/=) :: App -> App -> Bool
Show App Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> App -> ShowS show :: App -> String showList :: [App] -> ShowS
HTypeable App Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: App -> HType
XmlContent App Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser App toContents :: App -> [Content ()] xToChar :: App -> Char xFromChar :: Char -> App

data Abs Source #

Constructors

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

Instances

Instances details

Eq Abs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Abs -> Abs -> Bool (/=) :: Abs -> Abs -> Bool
Show Abs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Abs -> ShowS show :: Abs -> String showList :: [Abs] -> ShowS
HTypeable Abs Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Abs -> HType
XmlContent Abs Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Abs toContents :: Abs -> [Content ()] xToChar :: Abs -> Char xFromChar :: Char -> Abs

data Abs_Attrs Source #

Constructors

Abs_Attrs
Fields absVname :: String

Instances

Instances details

Eq Abs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Abs_Attrs -> Abs_Attrs -> Bool (/=) :: Abs_Attrs -> Abs_Attrs -> Bool
Show Abs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Abs_Attrs -> ShowS show :: Abs_Attrs -> String showList :: [Abs_Attrs] -> ShowS
XmlAttributes Abs_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Abs_Attrs toAttrs :: Abs_Attrs -> [Attribute]

data TVar Source #

Constructors

TVar TVar_Attrs [Class]

Instances

Instances details

Eq TVar Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: TVar -> TVar -> Bool (/=) :: TVar -> TVar -> Bool
Show TVar Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> TVar -> ShowS show :: TVar -> String showList :: [TVar] -> ShowS
HTypeable TVar Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: TVar -> HType
XmlContent TVar Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser TVar toContents :: TVar -> [Content ()] xToChar :: TVar -> Char xFromChar :: Char -> TVar

data TVar_Attrs Source #

Constructors

TVar_Attrs
Fields tVarName :: String tVarIndex :: Maybe String

Instances

Instances details

Eq TVar_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: TVar_Attrs -> TVar_Attrs -> Bool (/=) :: TVar_Attrs -> TVar_Attrs -> Bool
Show TVar_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> TVar_Attrs -> ShowS show :: TVar_Attrs -> String showList :: [TVar_Attrs] -> ShowS
XmlAttributes TVar_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> TVar_Attrs toAttrs :: TVar_Attrs -> [Attribute]

data TFree Source #

Constructors

TFree TFree_Attrs [Class]

Instances

Instances details

Eq TFree Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: TFree -> TFree -> Bool (/=) :: TFree -> TFree -> Bool
Show TFree Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> TFree -> ShowS show :: TFree -> String showList :: [TFree] -> ShowS
HTypeable TFree Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: TFree -> HType
XmlContent TFree Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser TFree toContents :: TFree -> [Content ()] xToChar :: TFree -> Char xFromChar :: Char -> TFree

data TFree_Attrs Source #

Constructors

TFree_Attrs
Fields tFreeName :: String

Instances

Instances details

Eq TFree_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: TFree_Attrs -> TFree_Attrs -> Bool (/=) :: TFree_Attrs -> TFree_Attrs -> Bool
Show TFree_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> TFree_Attrs -> ShowS show :: TFree_Attrs -> String showList :: [TFree_Attrs] -> ShowS
XmlAttributes TFree_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> TFree_Attrs toAttrs :: TFree_Attrs -> [Attribute]

data Type Source #

Constructors

Type Type_Attrs [OneOf3 TVar TFree Type]

Instances

Instances details

Eq Type Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Type -> Type -> Bool (/=) :: Type -> Type -> Bool
Show Type Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Type -> ShowS show :: Type -> String showList :: [Type] -> ShowS
HTypeable Type Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Type -> HType
XmlContent Type Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Type toContents :: Type -> [Content ()] xToChar :: Type -> Char xFromChar :: Char -> Type

data Type_Attrs Source #

Constructors

Type_Attrs
Fields typeName :: String

Instances

Instances details

Eq Type_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Type_Attrs -> Type_Attrs -> Bool (/=) :: Type_Attrs -> Type_Attrs -> Bool
Show Type_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Type_Attrs -> ShowS show :: Type_Attrs -> String showList :: [Type_Attrs] -> ShowS
XmlAttributes Type_Attrs Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Type_Attrs toAttrs :: Type_Attrs -> [Attribute]

data Class Source #

Constructors

Class
Fields className :: String

Instances

Instances details

Eq Class Source #
Instance details Defined in Isabelle.IsaExport Methods (==) :: Class -> Class -> Bool (/=) :: Class -> Class -> Bool
Show Class Source #
Instance details Defined in Isabelle.IsaExport Methods showsPrec :: Int -> Class -> ShowS show :: Class -> String showList :: [Class] -> ShowS
HTypeable Class Source #
Instance details Defined in Isabelle.IsaExport Methods toHType :: Class -> HType
XmlAttributes Class Source #
Instance details Defined in Isabelle.IsaExport Methods fromAttrs :: [Attribute] -> Class toAttrs :: Class -> [Attribute]
XmlContent Class Source #
Instance details Defined in Isabelle.IsaExport Methods parseContents :: XMLParser Class toContents :: Class -> [Content ()] xToChar :: Class -> Char xFromChar :: Char -> 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