--- a/src/ZF/Arith.ML Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/Arith.ML Fri Jan 29 17:08:20 1999 +0100
@@ -535,7 +535,7 @@
Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
-be rev_mp 1;
+by (etac rev_mp 1);
by (induct_tac "n" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
by (blast_tac (claset() addSEs [leE]
--- a/src/ZF/Epsilon.ML Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/Epsilon.ML Fri Jan 29 17:08:20 1999 +0100
@@ -217,8 +217,8 @@
Goal "rank(Pow(a)) = succ(rank(a))";
by (rtac (rank RS trans) 1);
by (rtac le_anti_sym 1);
-br UN_upper_le 2;
-br UN_least_le 1;
+by (rtac UN_upper_le 2);
+by (rtac UN_least_le 1);
by (auto_tac (claset() addIs [rank_mono], simpset()));
qed "rank_Pow";
--- a/src/ZF/ex/Limit.ML Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/ex/Limit.ML Fri Jan 29 17:08:20 1999 +0100
@@ -1425,7 +1425,7 @@
Goal "emb_chain(DD,ee) ==> cpo(Dinf(DD,ee))";
by (rtac subcpo_cpo 1);
-be subcpo_Dinf 1;
+by (etac subcpo_Dinf 1);
by (auto_tac (claset() addIs [cpo_iprod, emb_chain_cpo], simpset()));
qed "cpo_Dinf";
--- a/src/ZF/ex/Primrec.ML Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/ex/Primrec.ML Fri Jan 29 17:08:20 1999 +0100
@@ -159,7 +159,7 @@
\ i#+j < ack(succ(succ(succ(succ(k)))), j)";
by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
by (rtac (ack_add_bound RS lt_trans2) 2);
-br add_lt_mono 1;
+by (rtac add_lt_mono 1);
by Auto_tac;
qed "ack_add_bound2";
--- a/src/ZF/upair.ML Fri Jan 29 16:26:12 1999 +0100
+++ b/src/ZF/upair.ML Fri Jan 29 17:08:20 1999 +0100
@@ -230,8 +230,8 @@
by (rtac theI 1);
by (rtac classical 1);
by (resolve_tac prems 1);
-be (the_0 RS subst) 1;
-ba 1;
+by (etac (the_0 RS subst) 1);
+by (assume_tac 1);
qed "theI2";
(*** if -- a conditional expression for formulae ***)