--- a/Attic/Quot/Examples/FSet_BallBex.thy	Sat Sep 04 07:39:38 2010 +0800
+++ b/Attic/Quot/Examples/FSet_BallBex.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -11,15 +11,13 @@
   apply (metis mem_def)
   done
 
-(* Should not work and doesn't.
 thm test[quot_lifted]
-*)
 
 lemma "\<forall>xs \<in> (\<lambda>xs. x |\<in>| xs). x |\<in>| finsert y xs"
-  unfolding Ball_def mem_def
-  by (lifting test[unfolded Ball_def mem_def])
+  unfolding Ball_def
+  by (lifting test[unfolded Ball_def])
 
-ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def mem_def} @{thm test}*}
+ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def} @{thm test}*}
 
 lemma test2:
   "\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []"
@@ -27,14 +25,12 @@
   apply (auto simp add: mem_def)
   done
 
-(* Should not work and doesn't
 thm test2[quot_lifted]
-*)
 
 lemma "\<exists>xs \<in> (\<lambda>xs. xs = {||}). xs = {||}"
-  unfolding Bex_def mem_def
-  by (lifting test2[unfolded Bex_def mem_def])
+  unfolding Bex_def
+  by (lifting test2[unfolded Bex_def])
 
-ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def mem_def} @{thm test2}*}
+ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def} @{thm test2}*}
 
 end

--- a/Quotient-Paper/Paper.thy	Sat Sep 04 07:39:38 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -23,7 +23,7 @@
 notation (latex output)
   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
-  "op -->" (infix "\<longrightarrow>" 100) and
+  implies (infix "\<longrightarrow>" 100) and
   "==>" (infix "\<Longrightarrow>" 100) and
   fun_map ("_ \<singlearr> _" 51) and
   fun_rel ("_ \<doublearr> _" 51) and