<IsaExport file="example"><Consts><ConstDecl name="example.I"><Type name="example.type1"/><NoTerm/></ConstDecl></Consts><Axioms/><Theorems><Term name="example.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="example.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="type6"><RecType i="0" name="type6"><Vars><DtTFree s="&apos;a"/></Vars><Constructors><Constructor val="bar"><DtTFree s="&apos;a"/></Constructor></Constructors></RecType></TypeDecl><TypeDecl name="type1"><RecType i="0" name="type4"><Vars/><Constructors><Constructor val="foo"/><Constructor val="bar"><DtRec i="1"/></Constructor></Constructors></RecType><RecType i="1" name="type5"><Vars/><Constructors><Constructor val="nat * type1"/></Constructors></RecType><RecType i="2" name="type3"><Vars/><Constructors><Constructor val="nat * type2"/></Constructors></RecType></TypeDecl></Types></IsaExport>