--- a/src/ZF/Bool.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/Bool.ML Fri Nov 19 11:25:36 1993 +0100
@@ -29,7 +29,7 @@
val major::prems = goalw Bool.thy bool_defs
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P";
-br (major RS consE) 1;
+by (rtac (major RS consE) 1);
by (REPEAT (eresolve_tac (singletonE::prems) 1));
val boolE = result();
@@ -119,7 +119,7 @@
val and_absorb = result();
goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
-be boolE 1;
+by (etac boolE 1);
by (bool0_tac 1);
by (bool0_tac 1);
val and_commute = result();
@@ -142,7 +142,7 @@
val or_absorb = result();
goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
-be boolE 1;
+by (etac boolE 1);
by (bool0_tac 1);
by (bool0_tac 1);
val or_commute = result();
--- a/src/ZF/Epsilon.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/Epsilon.ML Fri Nov 19 11:25:36 1993 +0100
@@ -197,7 +197,7 @@
goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
-be (UN_I RS ltI) 1;
+by (etac (UN_I RS ltI) 1);
by (rtac succI1 1);
by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
val rank_lt = result();
@@ -236,7 +236,7 @@
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
by (etac succE 1);
by (fast_tac ZF_cs 1);
-be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
+by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
val rank_succ = result();
goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
--- a/src/ZF/QUniv.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/QUniv.ML Fri Nov 19 11:25:36 1993 +0100
@@ -99,8 +99,8 @@
(*The opposite inclusion*)
goalw QUniv.thy [quniv_def,QPair_def]
"!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
-be ([Transset_eclose RS Transset_univ, PowD] MRS
- Transset_includes_summands RS conjE) 1;
+by (etac ([Transset_eclose RS Transset_univ, PowD] MRS
+ Transset_includes_summands RS conjE) 1);
by (REPEAT (ares_tac [conjI,PowI] 1));
val quniv_QPair_D = result();
--- a/src/ZF/bool.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/bool.ML Fri Nov 19 11:25:36 1993 +0100
@@ -29,7 +29,7 @@
val major::prems = goalw Bool.thy bool_defs
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P";
-br (major RS consE) 1;
+by (rtac (major RS consE) 1);
by (REPEAT (eresolve_tac (singletonE::prems) 1));
val boolE = result();
@@ -119,7 +119,7 @@
val and_absorb = result();
goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
-be boolE 1;
+by (etac boolE 1);
by (bool0_tac 1);
by (bool0_tac 1);
val and_commute = result();
@@ -142,7 +142,7 @@
val or_absorb = result();
goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
-be boolE 1;
+by (etac boolE 1);
by (bool0_tac 1);
by (bool0_tac 1);
val or_commute = result();
--- a/src/ZF/epsilon.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/epsilon.ML Fri Nov 19 11:25:36 1993 +0100
@@ -197,7 +197,7 @@
goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
-be (UN_I RS ltI) 1;
+by (etac (UN_I RS ltI) 1);
by (rtac succI1 1);
by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
val rank_lt = result();
@@ -236,7 +236,7 @@
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
by (etac succE 1);
by (fast_tac ZF_cs 1);
-be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
+by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
val rank_succ = result();
goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
--- a/src/ZF/fin.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/fin.ML Fri Nov 19 11:25:36 1993 +0100
@@ -74,7 +74,7 @@
(*Every subset of a finite set is finite.*)
goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
-be Fin_induct 1;
+by (etac Fin_induct 1);
by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
--- a/src/ZF/func.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/func.ML Fri Nov 19 11:25:36 1993 +0100
@@ -260,7 +260,7 @@
val [prem] = goalw ZF.thy [restrict_def]
"A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
by (rtac (refl RS lam_cong) 1);
-be (prem RS subsetD RS beta) 1; (*easier than calling simp_tac*)
+by (etac (prem RS subsetD RS beta) 1); (*easier than calling simp_tac*)
val restrict_lam_eq = result();
--- a/src/ZF/quniv.ML Thu Nov 18 18:48:23 1993 +0100
+++ b/src/ZF/quniv.ML Fri Nov 19 11:25:36 1993 +0100
@@ -99,8 +99,8 @@
(*The opposite inclusion*)
goalw QUniv.thy [quniv_def,QPair_def]
"!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
-be ([Transset_eclose RS Transset_univ, PowD] MRS
- Transset_includes_summands RS conjE) 1;
+by (etac ([Transset_eclose RS Transset_univ, PowD] MRS
+ Transset_includes_summands RS conjE) 1);
by (REPEAT (ares_tac [conjI,PowI] 1));
val quniv_QPair_D = result();