# HG changeset patch
# User lcp
# Date 753704736 -3600
# Node ID dc50a4b96d7bcfaced9c61c05808b27037dd868b
# Parent  b0ec0c1bddb73ea474438bab6e3c38fd987b6cb8
expandshort and other trivial changes

diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/Bool.ML
--- 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();
diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/Epsilon.ML
--- 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))";
diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/QUniv.ML
--- 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();
 
diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/bool.ML
--- 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();
diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/epsilon.ML
--- 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))";
diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/fin.ML
--- 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);
diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/func.ML
--- 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();
 
 
diff -r b0ec0c1bddb7 -r dc50a4b96d7b src/ZF/quniv.ML
--- 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();