--- a/Quotient-Paper/Paper.thy	Thu Apr 28 11:51:01 2011 +0800
+++ b/Quotient-Paper/Paper.thy	Mon May 02 13:01:02 2011 +0800
@@ -1,6 +1,7 @@
 (*<*)
 theory Paper
-imports "Quotient" "Quotient_Syntax"
+imports "Quotient" 
+        "~~/src/HOL/Library/Quotient_Syntax"
         "~~/src/HOL/Library/LaTeXsugar"
         "~~/src/HOL/Quotient_Examples/FSet"
 begin
@@ -25,7 +26,7 @@
   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
   implies (infix "\<longrightarrow>" 100) and
   "==>" (infix "\<Longrightarrow>" 100) and
-  fun_map ("_ \<singlearr> _" 51) and
+  map_fun ("_ \<singlearr> _" 51) and
   fun_rel ("_ \<doublearr> _" 51) and
   list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
   empty_fset ("\<emptyset>") and
@@ -62,6 +63,15 @@
          (id ---> rep_fset ---> abs_fset) op #"
   by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
 
+lemma list_all2_symp:
+  assumes a: "equivp R"
+  and b: "list_all2 R xs ys"
+  shows "list_all2 R ys xs"
+using list_all2_lengthD[OF b] b
+apply(induct xs ys rule: list_induct2)
+apply(auto intro: equivp_symp[OF a])
+done
+
 lemma concat_rsp_unfolded:
   "\<lbrakk>list_all2 list_eq a ba; list_eq ba bb; list_all2 list_eq bb b\<rbrakk> \<Longrightarrow> list_eq (concat a) (concat b)"
 proof -
@@ -364,7 +374,7 @@
   also the following map for function types
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm fun_map_def[no_vars, THEN eq_reflection]}
+  @{thm map_fun_def[no_vars, THEN eq_reflection]}
   \end{isabelle}
 
   \noindent