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+
−
+
−
+
−
+
−