<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"><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="tt"><App><App><Const name="HOL.implies"><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="&apos;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="&apos;a"/></Vars><Constructors><Constructor val="a * nat * &apos;a type1"/></Constructors></RecType><RecType i="2" name="type3"><Vars><DtTFree s="&apos;a"/></Vars><Constructors><Constructor val="nat * &apos;a type2"/></Constructors></RecType></TypeDecl><TypeDecl name="type6"><RecType i="0" name="type6"><Vars><DtTFree s="&apos;a"/></Vars><Constructors><Constructor val="bar"><DtTFree s="&apos;a"/></Constructor></Constructors></RecType></TypeDecl></Types></IsaExport>