# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256219105 -7200
# Node ID 9c74171ff78b72dc3f80e20a9ae4a5fa489d3c95
# Parent  8b3d4806ad79f0bdc3b14614804b08fe5f814f84
The proof gets simplified

diff -r 8b3d4806ad79 -r 9c74171ff78b QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 15:44:16 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 15:45:05 2009 +0200
@@ -1035,7 +1035,7 @@
       instantiate_tac @{thm REP_ABS_RSP(1)} ctxt,
       instantiate_tac @{thm APPLY_RSP} ctxt,
       rtac reflex_thm,
-      Cong_Tac.cong_tac @{thm cong},
+(*      Cong_Tac.cong_tac @{thm cong},*)
       atac
     ])
 *}
@@ -1093,7 +1093,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 (* ABS_REP_RSP *)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
@@ -1153,7 +1152,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
@@ -1171,7 +1169,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 done