Documentation

type IsaData = (String, Maybe String, [String], [String], [String], [Sentence]) Source #

importIsaDataIO :: String -> IO [IsaData] Source #

importIsaData :: [Thy] -> [IsaData] Source #

hXmlBody_2IsaSentence :: Body_ -> Sentence Source #

hXmlCtxt2IsaCtxt :: Ctxt -> Ctxt Source #

hXmlMixfix2IsaMixfix :: Mixfix -> Mixfix Source #

hXmlOneOf4_2IsaMixfixTemplate :: OneOf4 Arg AString Break Block -> MixfixTemplate Source #

hXmlDatatype2IsaDatatype :: Datatype -> Datatype Source #

hXmlDomain2IsaDomain :: Domain -> Domain Source #

hXmlFixrecEquation2IsaFixrecEquation :: FixrecEquation -> FixrecEquation Source #

hXmlAxiom2IsaAxiom :: Axiom -> Axiom Source #

hXmlClass2IsaClass :: Class -> IsaClass Source #

hXmlSort2IsaSort :: Sort -> Sort Source #

hXmlType2IsaTyp :: Type -> Typ Source #

hXmlTFree2IsaTyp :: TFree -> Typ Source #

hXmlOneOf3_2IsaTyp :: OneOf3 TVar TFree Type -> Typ Source #

hXmlOneOf6_2IsaTerm :: [String] -> OneOf6 Bound Free Var Const App Abs -> Term Source #

hXmlConst2IsaTerm :: Const -> Term Source #

hXmlApp2IsaTerm :: [String] -> App -> Term Source #

hXmlAbs2IsaTerm :: [String] -> Abs -> Term Source #