--- a/Nominal/Ex/Classical.thy	Wed Jun 29 17:01:09 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Wed Jun 29 19:21:26 2011 +0100
@@ -2,6 +2,7 @@
 imports "../Nominal2"
 begin
 
+
 (* example from Urban's PhD *)
 
 atom_decl name
@@ -177,7 +178,9 @@
   then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c"
     apply(simp add: fresh_star_eqvt set_eqvt)
     sorry (* perm? *)
-  then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 apply (simp add: inter_eqvt)
+  then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 
+    apply (simp add: inter_eqvt)
+    sorry
   (* rest similar reversing it other way around... *)
   show ?thesis sorry
 qed
@@ -476,6 +479,8 @@
   apply(blast)
   done
 
+
+
 end