# HG changeset patch
# User paulson
# Date 864732371 -7200
# Node ID 13f1df323daf6d024701579398a69d96ebc9dd72
# Parent  c224dddc5f71c6e0bbd7eb34412cef6c3d313fc8
Restoration of the two "bypassed" theorems Union_quotient and quotient_disj

diff -r c224dddc5f71 -r 13f1df323daf src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Tue May 27 13:25:00 1997 +0200
+++ b/src/HOL/Integ/Equiv.ML	Tue May 27 13:26:11 1997 +0200
@@ -125,22 +125,19 @@
 by (Fast_tac 1);
 qed "quotientE";
 
-(** Not needed by Theory Integ --> bypassed **)
-(**goalw Equiv.thy [equiv_def,refl_def,quotient_def]
+goalw Equiv.thy [equiv_def,refl_def,quotient_def]
     "!!A r. equiv A r ==> Union(A/r) = A";
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [equalityI]) 1);
 qed "Union_quotient";
-**)
 
-(** Not needed by Theory Integ --> bypassed **)
-(*goalw Equiv.thy [quotient_def]
-    "!!A r. [| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y <= 0)";
+goalw Equiv.thy [quotient_def]
+    "!!A r. [| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y = {})";
 by (safe_tac (!claset addSIs [equiv_class_eq]));
 by (assume_tac 1);
 by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
-by (Fast_tac 1);
+by (blast_tac (!claset addSIs [equalityI]) 1);
 qed "quotient_disj";
-**)
+
 
 (**** Defining unary operations upon equivalence classes ****)