--- a/Nominal/ExLet.thy	Wed Mar 31 16:26:51 2010 +0200
+++ b/Nominal/ExLet.thy	Wed Mar 31 16:27:44 2010 +0200
@@ -13,6 +13,7 @@
 | Ap "trm" "trm"
 | Lm x::"name" t::"trm"  bind x in t
 | Lt a::"lts" t::"trm"   bind "bn a" in t
+(*| L a::"lts" t1::"trm" t2::"trm"  bind "bn a" in t1, bind "bn a" in t2*)
 and lts =
   Lnil
 | Lcons "name" "trm" "lts"
@@ -22,6 +23,9 @@
   "bn Lnil = []"
 | "bn (Lcons x t l) = (atom x) # (bn l)"
 
+
+thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros
+
 thm trm_lts.fv
 thm trm_lts.eq_iff
 thm trm_lts.bn
@@ -29,6 +33,7 @@
 thm trm_lts.induct[no_vars]
 thm trm_lts.inducts[no_vars]
 thm trm_lts.distinct
+(*thm trm_lts.supp*)
 thm trm_lts.fv[simplified trm_lts.supp(1-2)]
 
 primrec