example.isa revision b538e214277386123cb6f1ab0c99ae8fd3a03963
<IsaExport file="example"><Consts><ConstDecl name="I"><Type name="example.type1"><Type name="Nat.nat"/></Type><NoTerm/></ConstDecl></Consts><Axioms/><Theorems><Term name="I"><App><App><Const name="HOL.implies" infixr="-->" mixfix_i="25"><Type name="fun"><Type name="HOL.bool"/><Type name="fun"><Type name="HOL.bool"/><Type name="HOL.bool"/></Type></Type></Const><Var name="A"><Type name="HOL.bool"/></Var></App><Var name="A"><Type name="HOL.bool"/></Var></App></Term><Term name="same_ax"><App><Const name="HOL.All"><Type name="fun"><Type name="fun"><Type name="fun"><TVar name="'a"><class name="HOL.type"/></TVar><TVar name="'a"><class name="HOL.type"/></TVar></Type><Type name="HOL.bool"/></Type><Type name="HOL.bool"/></Type></Const><Abs vname="g1"><Type name="fun"><TVar name="'a"><class name="HOL.type"/></TVar><TVar name="'a"><class name="HOL.type"/></TVar></Type><App><Const name="HOL.All"><Type name="fun"><Type name="fun"><Type name="fun"><TVar name="'a"><class name="HOL.type"/></TVar><TVar name="'a"><class name="HOL.type"/></TVar></Type><Type name="HOL.bool"/></Type><Type name="HOL.bool"/></Type></Const><Abs vname="g2"><Type name="fun"><TVar name="'a"><class name="HOL.type"/></TVar><TVar name="'a"><class name="HOL.type"/></TVar></Type><App><Const name="HOL.All"><Type name="fun"><Type name="fun"><Type name="HOL.bool"/><Type name="HOL.bool"/></Type><Type name="HOL.bool"/></Type></Const><Abs vname="a"><Type name="HOL.bool"/><App><Const name="HOL.All"><Type name="fun"><Type name="fun"><Type name="HOL.bool"/><Type name="HOL.bool"/></Type><Type name="HOL.bool"/></Type></Const><Abs vname="b"><Type name="HOL.bool"/><App><App><Const name="HOL.implies" infixr="-->" mixfix_i="25"><Type name="fun"><Type name="HOL.bool"/><Type name="fun"><Type name="HOL.bool"/><Type name="HOL.bool"/></Type></Type></Const><App><App><Const name="HOL.conj" infixr="&" mixfix_i="35"><Type name="fun"><Type name="HOL.bool"/><Type name="fun"><Type name="HOL.bool"/><Type name="HOL.bool"/></Type></Type></Const><Bound index="1"/></App><App><Const name="HOL.Not"><Type name="fun"><Type name="HOL.bool"/><Type name="HOL.bool"/></Type></Const><Bound index="0"/></App></App></App><App><App><Const name="HOL.eq" infixl="=" mixfix_i="50"><Type name="fun"><Type name="fun"><TVar name="'a"><class name="HOL.type"/></TVar><TVar name="'a"><class name="HOL.type"/></TVar></Type><Type name="fun"><Type name="fun"><TVar name="'a"><class name="HOL.type"/></TVar><TVar name="'a"><class name="HOL.type"/></TVar></Type><Type name="HOL.bool"/></Type></Type></Const><Bound index="3"/></App><Bound index="2"/></App></App></Abs></App></Abs></App></Abs></App></Abs></App></Term><Term name="tt"><App><App><Const name="HOL.implies" infixr="-->" mixfix_i="25"><Type name="fun"><Type name="HOL.bool"/><Type name="fun"><Type name="HOL.bool"/><Type name="HOL.bool"/></Type></Type></Const><Var name="test"><Type name="HOL.bool"/></Var></App><Var name="test"><Type name="HOL.bool"/></Var></App></Term></Theorems><Types><TypeDecl name="type1"><RecType i="0" name="type1" altname="type4"><Vars><DtTFree s="'a"/></Vars><Constructors><Constructor val="foo"/><Constructor val="bar"><DtRec i="1"/></Constructor></Constructors></RecType><RecType i="1" name="type2" altname="type5"><Vars><DtTFree s="'a"/></Vars><Constructors><Constructor val="a * nat * 'a type1"/></Constructors></RecType><RecType i="2" name="type3"><Vars><DtTFree s="'a"/></Vars><Constructors><Constructor val="nat * 'a type2"/></Constructors></RecType></TypeDecl><TypeDecl name="type6"><RecType i="0" name="type6"><Vars><DtTFree s="'a"/></Vars><Constructors><Constructor val="bar"><DtTFree s="'a"/></Constructor></Constructors></RecType></TypeDecl></Types></IsaExport>