--- a/Nominal/Ex/Lambda.thy	Wed May 19 12:29:08 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri May 21 10:45:29 2010 +0200
@@ -503,18 +503,16 @@
   apply simp
   apply (rule conjI)
   apply clarify
-  sorry
+  oops
 
-thm supp_at_base
 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)"
-  sorry
+  oops
 
 lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)"
   apply (induct t arbitrary: p y s)
   apply simp_all
   apply(perm_simp)
-  apply simp
-  sorry
+  oops
 
 lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x"
   apply (induct x arbitrary: d)
@@ -554,6 +552,12 @@
   apply (simp add: alpha_lam_raw.intros)
   apply simp
   apply (rule alpha_lam_raw.intros)
+  apply (rule_tac x="((new (insert (atom y) (fv_lam_raw a \<union> fv_lam_raw c) -
+                       {atom name}))\<leftrightarrow>(new (insert (atom y) (fv_lam_raw b \<union> fv_lam_raw c) -
+                        {atom name})))" in exI)
+  apply (simp only: alphas)
+  apply (tactic {* split_conj_tac 1 *})
+  prefer 3
   sorry
 
 lemma [quot_respect]:
@@ -576,7 +580,6 @@
   apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) -
                     {atom x})))" in exI)
   apply (simp only: alphas)
-  apply simp
   sorry
 
 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars]