diff -r cfd3a7368543 -r 3832a31a73b1 Nominal/ExLet.thy --- 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