src/HOL/Integ/Equiv.ML
changeset 1844 791e79473966
parent 1642 21db0cf9a1a4
child 1894 c2c8279d40f0
     1.1 --- a/src/HOL/Integ/Equiv.ML	Fri Jun 28 15:29:39 1996 +0200
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Jun 28 15:30:55 1996 +0200
     1.3 @@ -129,7 +129,7 @@
     1.4  (** Not needed by Theory Integ --> bypassed **)
     1.5  (**goalw Equiv.thy [equiv_def,refl_def,quotient_def]
     1.6      "!!A r. equiv A r ==> Union(A/r) = A";
     1.7 -by (fast_tac eq_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "Union_quotient";
    1.10  **)
    1.11  
    1.12 @@ -147,7 +147,7 @@
    1.13  
    1.14  (* theorem needed to prove UN_equiv_class *)
    1.15  goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
    1.16 -by (fast_tac (eq_cs addSEs [equalityE]) 1);
    1.17 +by (fast_tac (!claset addSEs [equalityE]) 1);
    1.18  qed "UN_singleton_lemma";
    1.19  val UN_singleton = ballI RSN (2,UN_singleton_lemma);
    1.20