# HG changeset patch
# User lcp
# Date 785422020 -3600
# Node ID 82caba9e130f51aef4f2305414d43604ccfaec61
# Parent  237456d216a536f8f12392603c6143b47d8ac56d
ZF/EquivClass/congruent_commuteI: uncommented and simplified proof

diff -r 237456d216a5 -r 82caba9e130f src/ZF/EquivClass.ML
--- a/src/ZF/EquivClass.ML	Mon Nov 21 13:09:41 1994 +0100
+++ b/src/ZF/EquivClass.ML	Mon Nov 21 13:47:00 1994 +0100
@@ -246,23 +246,19 @@
      ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
 val congruent2_commuteI = result();
 
-(***OBSOLETE VERSION
-(*Rules congruentI and congruentD would simplify use of rewriting below*)
+(*Obsolete?*)
 val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def]
     "[| equiv(A,r);  Z: A/r;  \
 \       !!w. [| w: A |] ==> congruent(r, %z.b(w,z));	\
 \       !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)	\
 \    |] ==> congruent(r, %w. UN z: Z. b(w,z))";
 val congt' = rewrite_rule [congruent_def] congt;
-by (cut_facts_tac [ZinA,congt] 1);
+by (cut_facts_tac [ZinA] 1);
 by (rewtac congruent_def);
 by (safe_tac ZF_cs);
 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
-by (asm_simp_tac (ZF_ss addsimps [congt RS (equivA RS UN_equiv_class)]) 1);
-by (rtac (commute RS trans) 1);
-by (rtac (commute RS trans RS sym) 3);
-by (rtac sym 5);
+by (asm_simp_tac (ZF_ss addsimps [commute,
+				  [equivA, congt] MRS UN_equiv_class]) 1);
 by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
 val congruent_commuteI = result();
-***)