theory SingleLet+ −
imports "../NewParser"+ −
begin+ −
+ −
atom_decl name+ −
+ −
declare [[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 y+ −
and 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.fv+ −
thm trm_assg.supp+ −
thm trm_assg.eq_iff+ −
thm trm_assg.bn+ −
thm trm_assg.perm+ −
thm trm_assg.induct+ −
thm trm_assg.inducts+ −
thm trm_assg.distinct+ −
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}+ −
+ −
(* TEMPORARY+ −
thm trm_assg.fv[simplified trm_assg.supp(1-2)]+ −
*)+ −
+ −
end+ −
+ −
+ −
+ −