theory SingleLetimports "../NewParser"beginatom_decl namedeclare [[STEPS = 9]]nominal_datatype trm = Var "name"| App "trm" "trm"| Lam x::"name" t::"trm" bind_set x in t| Let a::"assg" t::"trm" bind_set "bn a" in t| Foo x::"name" y::"name" t::"trm" bind_set x in y t| Bar x::"name" y::"name" t::"trm" bind y x in t x yand assg = As "name" "name" "trm" "name"binder bn::"assg \<Rightarrow> atom set"where "bn (As x y t z) = {atom x}"ML {* Inductive.the_inductive *}thm trm_assg.fvthm trm_assg.suppthm trm_assg.eq_iffthm trm_assg.bnthm trm_assg.permthm trm_assg.inductthm trm_assg.inductsthm trm_assg.distinctML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}(* TEMPORARYthm trm_assg.fv[simplified trm_assg.supp(1-2)]*)end