--- a/src/ZF/Cardinal.ML Wed Feb 02 12:25:29 2000 +0100
+++ b/src/ZF/Cardinal.ML Wed Feb 02 12:25:54 2000 +0100
@@ -517,7 +517,7 @@
Goalw [lesspoll_def] "[| A lesspoll i; Ord(i) |] ==> |A| < i";
by (Clarify_tac 1);
-by (forward_tac [lepoll_cardinal_le] 1);
+by (ftac lepoll_cardinal_le 1);
by (assume_tac 1);
by (blast_tac (claset() addIs [well_ord_Memrel,
well_ord_cardinal_eqpoll RS eqpoll_sym]
--- a/src/ZF/Finite.ML Wed Feb 02 12:25:29 2000 +0100
+++ b/src/ZF/Finite.ML Wed Feb 02 12:25:54 2000 +0100
@@ -183,8 +183,8 @@
(subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1);
by (fast_tac (claset() addDs
[FiniteFun_domain_Fin, Fin.dom_subset RS subsetD]) 1);
-by (resolve_tac [fun_FiniteFunI] 1);
-be FiniteFun_domain_Fin 1;
+by (rtac fun_FiniteFunI 1);
+by (etac FiniteFun_domain_Fin 1);
by (res_inst_tac [("B" , "range(f)")] fun_weaken_type 1);
by (ALLGOALS
(blast_tac (claset() addDs
--- a/src/ZF/upair.ML Wed Feb 02 12:25:29 2000 +0100
+++ b/src/ZF/upair.ML Wed Feb 02 12:25:54 2000 +0100
@@ -209,7 +209,7 @@
Goal "EX! x. P(x) ==> P(THE x. P(x))";
by (etac ex1E 1);
-by (rtac (the_equality RS ssubst) 1);
+by (stac the_equality 1);
by (REPEAT (Blast_tac 1));
qed "theI";