--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/SingleLet.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -0,0 +1,38 @@
+theory SingleLet
+imports "../Parser"
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := false *}
+
+nominal_datatype trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  bind x in t
+| Let a::"assg" t::"trm"  bind "bn a" in t
+and assg =
+  As "name" "trm"
+binder
+  bn::"assg \<Rightarrow> atom set"
+where
+  "bn (As x t) = {atom x}"
+
+print_theorems
+thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
+
+thm trm_assg.fv
+thm trm_assg.supp
+thm trm_assg.eq_iff[simplified alphas_abs[symmetric]]
+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}) *}
+thm trm_assg.fv[simplified trm_assg.supp]
+
+end
+
+
+