Removed a use of eq_cs
authorpaulson
Fri Jun 28 15:30:55 1996 +0200 (1996-06-28)
changeset 1844791e79473966
parent 1843 a6d7aef48c2f
child 1845 afa622bc829d
Removed a use of eq_cs
src/HOL/IOA/meta_theory/IOA.ML
src/HOL/Integ/Equiv.ML
     1.1 --- a/src/HOL/IOA/meta_theory/IOA.ML	Fri Jun 28 15:29:39 1996 +0200
     1.2 +++ b/src/HOL/IOA/meta_theory/IOA.ML	Fri Jun 28 15:30:55 1996 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  "actions(asig_comp a b) = actions(a) Un actions(b)";
     1.5    by(simp_tac (!simpset addsimps
     1.6                 ([actions_def,asig_comp_def]@asig_projections)) 1);
     1.7 -  by(fast_tac eq_cs 1);
     1.8 +  by(Fast_tac 1);
     1.9  qed "actions_asig_comp";
    1.10  
    1.11  goal IOA.thy
     2.1 --- a/src/HOL/Integ/Equiv.ML	Fri Jun 28 15:29:39 1996 +0200
     2.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Jun 28 15:30:55 1996 +0200
     2.3 @@ -129,7 +129,7 @@
     2.4  (** Not needed by Theory Integ --> bypassed **)
     2.5  (**goalw Equiv.thy [equiv_def,refl_def,quotient_def]
     2.6      "!!A r. equiv A r ==> Union(A/r) = A";
     2.7 -by (fast_tac eq_cs 1);
     2.8 +by (Fast_tac 1);
     2.9  qed "Union_quotient";
    2.10  **)
    2.11  
    2.12 @@ -147,7 +147,7 @@
    2.13  
    2.14  (* theorem needed to prove UN_equiv_class *)
    2.15  goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
    2.16 -by (fast_tac (eq_cs addSEs [equalityE]) 1);
    2.17 +by (fast_tac (!claset addSEs [equalityE]) 1);
    2.18  qed "UN_singleton_lemma";
    2.19  val UN_singleton = ballI RSN (2,UN_singleton_lemma);
    2.20