--- a/src/ZF/Order.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Order.ML Wed Jan 08 15:04:27 1997 +0100
@@ -82,13 +82,13 @@
goalw Order.thy [pred_def]
"pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "pred_pred_eq";
goalw Order.thy [trans_on_def, pred_def]
"!!r. [| trans[A](r); <y,x>:r; x:A; y:A \
\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "trans_pred_pred_eq";
@@ -171,7 +171,7 @@
qed "tot_ord_0";
goalw Order.thy [wf_on_def, wf_def] "wf[0](r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
qed "wf_on_0";
goalw Order.thy [well_ord_def] "well_ord(0,r)";
@@ -300,7 +300,7 @@
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, ord_iso_def]
"!!A B r. [| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)";
by (Asm_simp_tac 1);
-by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1);
+by (fast_tac (!claset addIs [bij_is_fun RS apply_type]) 1);
qed "part_ord_ord_iso";
goalw Order.thy [linear_def, ord_iso_def]
@@ -319,11 +319,10 @@
by (asm_full_simp_tac (!simpset addcongs [conj_cong2]) 1);
by (safe_tac (!claset));
by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
-by (safe_tac eq_cs);
+by (safe_tac (!claset addSIs [equalityI]));
by (dtac equalityD1 1);
by (fast_tac (!claset addSIs [bexI]) 1);
-by (fast_tac (!claset addSIs [bexI]
- addIs [bij_is_fun RS apply_type]) 1);
+by (fast_tac (!claset addSIs [bexI] addIs [bij_is_fun RS apply_type]) 1);
qed "wf_on_ord_iso";
goalw Order.thy [well_ord_def, tot_ord_def]
@@ -382,7 +381,8 @@
by (etac CollectE 1);
by (asm_simp_tac
(!simpset addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
-by (safe_tac (eq_cs addSEs [bij_is_fun RS apply_type]));
+by (rtac equalityI 1);
+by (safe_tac (!claset addSEs [bij_is_fun RS apply_type]));
by (rtac RepFun_eqI 1);
by (fast_tac (!claset addSIs [right_inverse_bij RS sym]) 1);
by (asm_simp_tac bij_inverse_ss 1);
@@ -472,7 +472,7 @@
goalw Order.thy [ord_iso_map_def]
"converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
-by (fast_tac (eq_cs addIs [ord_iso_sym]) 1);
+by (fast_tac (!claset addIs [ord_iso_sym]) 1);
qed "converse_ord_iso_map";
goalw Order.thy [ord_iso_map_def, function_def]