--- a/Nominal/Ex/SingleLet.thy	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Fri Jun 11 03:02:42 2010 +0200
@@ -2,10 +2,10 @@
 imports "../NewParser"
 begin
 
-
 atom_decl name
 
-declare [[STEPS = 11]]
+declare [[STEPS = 12]]
+
 
 nominal_datatype trm =
   Var "name"
@@ -14,6 +14,7 @@
 | Let a::"assg" t::"trm"  bind_set "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
+| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
 and assg =
   As "name" "name" "trm" "name"
 binder
@@ -22,6 +23,48 @@
   "bn (As x y t z) = {atom x}"
 
 
+lemma
+  shows "alpha_trm_raw x x"
+  and "alpha_assg_raw y y"
+  and "alpha_bn_raw y y"
+apply(induct rule: trm_raw_assg_raw.inducts)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule refl)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(assumption)
+apply(assumption)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(assumption)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(assumption)
+apply(assumption)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(simp only: prod_alpha_def split_conv prod_rel.simps)
+apply(simp)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(simp only: prod_alpha_def split_conv prod_rel.simps)
+apply(simp)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule refl)
+apply(rule refl)
+apply(assumption)
+apply(rule refl)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule refl)
+apply(assumption)
+apply(rule refl)
+done
+
+
+
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff