--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/ExLetMult.thy	Sat Apr 03 22:31:11 2010 +0200
@@ -0,0 +1,31 @@
+theory ExLetMult
+imports "../Parser"
+begin
+
+atom_decl name
+
+ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaLst *}
+ML {* val _ = cheat_equivp := true *}
+nominal_datatype trm =
+  Vr "name"
+| Ap "trm" "trm"
+| Lm x::"name" t::"trm" bind x in t
+| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t, bind "bn l" in s
+and lts =
+  Lnil
+| Lcons "name" "trm" "lts"
+binder
+  bn
+where
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
+
+thm trm_lts.eq_iff
+thm trm_lts.induct
+thm trm_lts.fv[simplified trm_lts.supp]
+
+end
+
+
+