--- a/Nominal/Test.thy	Wed Mar 03 12:48:05 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 14:22:58 2010 +0100
@@ -14,42 +14,6 @@
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
-lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)"
-apply (erule alpha_weird_raw.induct)
-defer
-apply (simp add: alpha_weird_raw.intros)
-apply (simp add: alpha_weird_raw.intros)
-apply (simp only: permute_weird_raw.simps)
-apply (rule alpha_weird_raw.intros)
-apply (erule exi[of _ _ "p"])
-apply (erule exi[of _ _ "p"])
-apply (erule exi[of _ _ "p"])
-apply (erule exi[of _ _ "p"])
-apply (erule conjE)+
-apply (rule conjI)
-apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
-apply (simp add: eqvts)
-apply (simp add: eqvts)
-apply (rule conjI)
-defer
-apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
-apply (simp add: eqvts)
-apply (simp add: eqvts)
-apply (rule conjI)
-defer
-apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt)
-apply(simp add: alpha_gen.simps)
-apply(erule conjE)+
-  apply(rule conjI)
-  apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
-apply (simp add: eqvts)
-  apply(rule conjI)
-  apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
-apply (simp add: eqvts add_perm_eqvt)
-apply (simp add: permute_eqvt[symmetric])
-done
-
-
 (*
 abbreviation "WBind \<equiv> WBind_raw"
 abbreviation "WP \<equiv> WP_raw"