src/ZF/Ordinal.ML

 goalw Ordinal.thy [Transset_def] "Transset(A) <-> A<=Pow(A)";
 by (Fast_tac 1);
 qed "Transset_iff_Pow";
 
 goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "Transset_iff_Union_succ";
 
 (** Consequences of downwards closure **)
 
 goalw Ordinal.thy [Transset_def]

 goalw Ordinal.thy [Memrel_def] "!!A B. A<=B ==> Memrel(A) <= Memrel(B)";
 by (Fast_tac 1);
 qed "Memrel_mono";
 
 goalw Ordinal.thy [Memrel_def] "Memrel(0) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Memrel_0";
 
 goalw Ordinal.thy [Memrel_def] "Memrel(1) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Memrel_1";
 
 Addsimps [Memrel_0, Memrel_1];
 
 (*The membership relation (as a set) is well-founded.

 val prems = goal Ordinal.thy
     "Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)";
 by (trans_ind_tac "i" prems 1);
 by (rtac (impI RS allI) 1);
 by (trans_ind_tac "j" [] 1);
-by (DEPTH_SOLVE (step_tac eq_cs 1 ORELSE Ord_trans_tac 1));
+by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1));
 qed "Ord_linear_lemma";
 
 (*"[| Ord(i); Ord(x) |] ==> i:x | i=x | x:i"*)
 bind_thm ("Ord_linear", Ord_linear_lemma RS spec RS mp);
 

 by (REPEAT (eresolve_tac [asm_rl, leprem RS ltE] 1
      ORELSE dtac Ord_succD 1));
 qed "le_implies_UN_le_UN";
 
 goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
-by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+by (fast_tac (!claset addEs [Ord_trans]) 1);
 qed "Ord_equality";
 
 (*Holds for all transitive sets, not just ordinals*)
 goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i";
 by (fast_tac (!claset addSEs [Ord_trans]) 1);

 
 
 (*** Limit ordinals -- general properties ***)
 
 goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
-by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
+by (fast_tac (!claset addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
 qed "Limit_Union_eq";
 
 goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
 by (etac conjunct1 1);
 qed "Limit_is_Ord";

 
 (** Traditional 3-way case analysis on ordinals **)
 
 goal Ordinal.thy "!!i. Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)";
 by (fast_tac (!claset addSIs [non_succ_LimitI, Ord_0_lt]
-         	      addSDs [Ord_succD]) 1);
+                      addSDs [Ord_succD]) 1);
 qed "Ord_cases_disj";
 
 val major::prems = goal Ordinal.thy
     "[| Ord(i);                 \
 \       i=0                          ==> P;     \