diff -r e801b929216b -r 6a51704204e5 QuotMain.thy
--- a/QuotMain.thy	Mon Sep 28 19:22:28 2009 +0200
+++ b/QuotMain.thy	Mon Sep 28 19:24:55 2009 +0200
@@ -565,7 +565,7 @@
 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
 
-lemma list_eq_sym:
+lemma list_eq_refl:
   shows "xs \<approx> xs"
   apply (induct xs)
    apply (auto intro: list_eq.intros)
@@ -574,7 +574,7 @@
 lemma equiv_list_eq:
   shows "EQUIV list_eq"
   unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
-  apply(auto intro: list_eq.intros list_eq_sym)
+  apply(auto intro: list_eq.intros list_eq_refl)
   done
 
 local_setup {*
@@ -693,7 +693,7 @@
   using c 
 apply(induct xs)
 apply (metis Suc_neq_Zero card1_0)
-apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons)
+apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)
 done
 
 lemma cons_preserves:
@@ -773,7 +773,7 @@
 apply(rule list_eq.intros(3))
 apply(unfold REP_fset_def ABS_fset_def)
 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
-apply(rule list_eq_sym)
+apply(rule list_eq_refl)
 done
 
 lemma append_respects_fst:
@@ -782,7 +782,7 @@
   using a
   apply(induct)
   apply(auto intro: list_eq.intros)
-  apply(simp add: list_eq_sym)
+  apply(simp add: list_eq_refl)
 done
 
 lemma yyy:
@@ -800,17 +800,17 @@
   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule append_respects_fst)
   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_sym)
+  apply(rule list_eq_refl)
   apply(simp)
   apply(rule_tac f="(op =)" in arg_cong2)
   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule append_respects_fst)
   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_sym)
+  apply(rule list_eq_refl)
   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule list_eq.intros(5))
   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_sym)
+  apply(rule list_eq_refl)
 done
 
 lemma
@@ -935,7 +935,7 @@
   fun foo_tac' ctxt =
     REPEAT_ALL_NEW (FIRST' [
       rtac @{thm trueprop_cong},
-      rtac @{thm list_eq_sym},
+      rtac @{thm list_eq_refl},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
@@ -1097,3 +1097,4 @@
 *)
 
 
+yyes
\ No newline at end of file