--- a/Nominal/Ex/ExLetMult.thy	Wed Aug 25 23:16:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-theory ExLetMult
-imports "../NewParser"
-begin
-
-atom_decl name
-
-nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind_set x in t
-| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t 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
-
-
-