# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1250855780 -7200
# Node ID b3d878d19a0976b631c01dbf06ebf3386917f2f2
# Parent  0eb89a350f434d0641baec49249c7104f4a2835d
Fixed

diff -r 0eb89a350f43 -r b3d878d19a09 QuotMain.thy
--- a/QuotMain.thy	Fri Aug 21 13:36:58 2009 +0200
+++ b/QuotMain.thy	Fri Aug 21 13:56:20 2009 +0200
@@ -70,12 +70,6 @@
 apply(simp add: thm10 thm11)
 done
 
-lemma REP_ABS_rsp:
-  shows "R g g \<Longrightarrow> (REP (ABS g) = g"
-apply(subst thm11)
-apply(simp add: thm10 thm11)
-done
-
 lemma QUOTIENT:
   "QUOTIENT R ABS REP"
 apply(unfold QUOTIENT_def)
@@ -567,7 +561,7 @@
 unfolding IN_def EMPTY_def
 apply(rule_tac f="(op =) False" in arg_cong)
 apply(rule mem_respects)
-apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
         simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 apply(rule list_eq.intros)
 done
@@ -589,7 +583,7 @@
 apply(rule mem_respects)
 apply(rule list_eq.intros(3))
 apply(unfold REP_fset_def ABS_fset_def)
-apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 apply(rule list_eq_sym)
 done
 
@@ -602,8 +596,6 @@
   apply(simp add: list_eq_sym)
 done
 
-thm list_eq.intros
-
 lemma yyy :
   shows "
     (
@@ -620,7 +612,7 @@
                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule helper)
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+  apply(simp only:QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
                     simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
   apply(simp)
@@ -629,14 +621,14 @@
                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule helper)
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
+  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
                      simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule list_eq.intros(5))
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
                  simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
 done