--- a/Nominal/Test.thy	Wed Mar 03 14:22:58 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 03 14:46:14 2010 +0100
@@ -14,37 +14,38 @@
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
-(*
+
 abbreviation "WBind \<equiv> WBind_raw"
 abbreviation "WP \<equiv> WP_raw"
 abbreviation "WV \<equiv> WV_raw"
 
 lemma test:
   assumes a: "distinct [x, y, z]"
-  shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))  
-                     (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
-apply(rule_tac alpha_weird.intros)
+  shows "alpha_weird_raw (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))  
+                         (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
+apply(rule_tac alpha_weird_raw.intros)
 unfolding alpha_gen
 using a
-apply(simp)
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply(auto)
 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply(auto)
+apply(simp add: fresh_star_def flip_def fresh_def supp_swap)
+apply(rule alpha_weird_raw.intros)
+apply(simp add: alpha_weird_raw.intros(2))
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply(rule_tac x="0" in exI)
 apply(simp add: fresh_star_def)
-apply(simp add: flip_def)
 apply(auto)
-prefer 2
-apply(rule alpha_weird.intros)
-apply(simp add: alpha_weird.intros(2))
-prefer 2
-apply(rule alpha_weird.intros)
-apply(simp add: alpha_weird.intros(2))
+apply(rule alpha_weird_raw.intros)
+apply(simp add: alpha_weird_raw.intros(2))
+apply(simp add: flip_def supp_swap supp_perm)
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply(simp)
-apply(rule alpha_weird.intros)
-apply(simp)
-apply(simp add: alpha_gen)
-using a
-apply(simp)
-*)
+apply(auto)
+apply(simp add: flip_def fresh_def supp_swap)
+apply(rule alpha_weird_raw.intros)
+apply(simp add: alpha_weird_raw.intros(2))
+done
 
 text {* example 1 *}