--- a/Nominal/ExLetMult.thy	Sat Apr 03 21:53:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-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
-
-
-