expandshort and other trivial changes
authorlcp
Fri Nov 19 11:25:36 1993 +0100 (1993-11-19)
changeset 129dc50a4b96d7b
parent 128 b0ec0c1bddb7
child 130 c035b6b9eafc
expandshort and other trivial changes
src/ZF/Bool.ML
src/ZF/Epsilon.ML
src/ZF/QUniv.ML
src/ZF/bool.ML
src/ZF/epsilon.ML
src/ZF/fin.ML
src/ZF/func.ML
src/ZF/quniv.ML
     1.1 --- a/src/ZF/Bool.ML	Thu Nov 18 18:48:23 1993 +0100
     1.2 +++ b/src/ZF/Bool.ML	Fri Nov 19 11:25:36 1993 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  val major::prems = goalw Bool.thy bool_defs
     1.6      "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
     1.7 -br (major RS consE) 1;
     1.8 +by (rtac (major RS consE) 1);
     1.9  by (REPEAT (eresolve_tac (singletonE::prems) 1));
    1.10  val boolE = result();
    1.11  
    1.12 @@ -119,7 +119,7 @@
    1.13  val and_absorb = result();
    1.14  
    1.15  goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
    1.16 -be boolE 1;
    1.17 +by (etac boolE 1);
    1.18  by (bool0_tac 1);
    1.19  by (bool0_tac 1);
    1.20  val and_commute = result();
    1.21 @@ -142,7 +142,7 @@
    1.22  val or_absorb = result();
    1.23  
    1.24  goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
    1.25 -be boolE 1;
    1.26 +by (etac boolE 1);
    1.27  by (bool0_tac 1);
    1.28  by (bool0_tac 1);
    1.29  val or_commute = result();
     2.1 --- a/src/ZF/Epsilon.ML	Thu Nov 18 18:48:23 1993 +0100
     2.2 +++ b/src/ZF/Epsilon.ML	Fri Nov 19 11:25:36 1993 +0100
     2.3 @@ -197,7 +197,7 @@
     2.4  
     2.5  goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
     2.6  by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
     2.7 -be (UN_I RS ltI) 1;
     2.8 +by (etac (UN_I RS ltI) 1);
     2.9  by (rtac succI1 1);
    2.10  by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
    2.11  val rank_lt = result();
    2.12 @@ -236,7 +236,7 @@
    2.13  by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
    2.14  by (etac succE 1);
    2.15  by (fast_tac ZF_cs 1);
    2.16 -be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
    2.17 +by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
    2.18  val rank_succ = result();
    2.19  
    2.20  goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
     3.1 --- a/src/ZF/QUniv.ML	Thu Nov 18 18:48:23 1993 +0100
     3.2 +++ b/src/ZF/QUniv.ML	Fri Nov 19 11:25:36 1993 +0100
     3.3 @@ -99,8 +99,8 @@
     3.4  (*The opposite inclusion*)
     3.5  goalw QUniv.thy [quniv_def,QPair_def]
     3.6      "!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
     3.7 -be ([Transset_eclose RS Transset_univ, PowD] MRS 
     3.8 -    Transset_includes_summands RS conjE) 1;
     3.9 +by (etac ([Transset_eclose RS Transset_univ, PowD] MRS 
    3.10 +	  Transset_includes_summands RS conjE) 1);
    3.11  by (REPEAT (ares_tac [conjI,PowI] 1));
    3.12  val quniv_QPair_D = result();
    3.13  
     4.1 --- a/src/ZF/bool.ML	Thu Nov 18 18:48:23 1993 +0100
     4.2 +++ b/src/ZF/bool.ML	Fri Nov 19 11:25:36 1993 +0100
     4.3 @@ -29,7 +29,7 @@
     4.4  
     4.5  val major::prems = goalw Bool.thy bool_defs
     4.6      "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
     4.7 -br (major RS consE) 1;
     4.8 +by (rtac (major RS consE) 1);
     4.9  by (REPEAT (eresolve_tac (singletonE::prems) 1));
    4.10  val boolE = result();
    4.11  
    4.12 @@ -119,7 +119,7 @@
    4.13  val and_absorb = result();
    4.14  
    4.15  goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
    4.16 -be boolE 1;
    4.17 +by (etac boolE 1);
    4.18  by (bool0_tac 1);
    4.19  by (bool0_tac 1);
    4.20  val and_commute = result();
    4.21 @@ -142,7 +142,7 @@
    4.22  val or_absorb = result();
    4.23  
    4.24  goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
    4.25 -be boolE 1;
    4.26 +by (etac boolE 1);
    4.27  by (bool0_tac 1);
    4.28  by (bool0_tac 1);
    4.29  val or_commute = result();
     5.1 --- a/src/ZF/epsilon.ML	Thu Nov 18 18:48:23 1993 +0100
     5.2 +++ b/src/ZF/epsilon.ML	Fri Nov 19 11:25:36 1993 +0100
     5.3 @@ -197,7 +197,7 @@
     5.4  
     5.5  goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
     5.6  by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
     5.7 -be (UN_I RS ltI) 1;
     5.8 +by (etac (UN_I RS ltI) 1);
     5.9  by (rtac succI1 1);
    5.10  by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
    5.11  val rank_lt = result();
    5.12 @@ -236,7 +236,7 @@
    5.13  by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
    5.14  by (etac succE 1);
    5.15  by (fast_tac ZF_cs 1);
    5.16 -be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
    5.17 +by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
    5.18  val rank_succ = result();
    5.19  
    5.20  goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
     6.1 --- a/src/ZF/fin.ML	Thu Nov 18 18:48:23 1993 +0100
     6.2 +++ b/src/ZF/fin.ML	Fri Nov 19 11:25:36 1993 +0100
     6.3 @@ -74,7 +74,7 @@
     6.4  
     6.5  (*Every subset of a finite set is finite.*)
     6.6  goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
     6.7 -be Fin_induct 1;
     6.8 +by (etac Fin_induct 1);
     6.9  by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
    6.10  by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
    6.11  by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
     7.1 --- a/src/ZF/func.ML	Thu Nov 18 18:48:23 1993 +0100
     7.2 +++ b/src/ZF/func.ML	Fri Nov 19 11:25:36 1993 +0100
     7.3 @@ -260,7 +260,7 @@
     7.4  val [prem] = goalw ZF.thy [restrict_def]
     7.5      "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
     7.6  by (rtac (refl RS lam_cong) 1);
     7.7 -be (prem RS subsetD RS beta) 1;	(*easier than calling simp_tac*)
     7.8 +by (etac (prem RS subsetD RS beta) 1);	(*easier than calling simp_tac*)
     7.9  val restrict_lam_eq = result();
    7.10  
    7.11  
     8.1 --- a/src/ZF/quniv.ML	Thu Nov 18 18:48:23 1993 +0100
     8.2 +++ b/src/ZF/quniv.ML	Fri Nov 19 11:25:36 1993 +0100
     8.3 @@ -99,8 +99,8 @@
     8.4  (*The opposite inclusion*)
     8.5  goalw QUniv.thy [quniv_def,QPair_def]
     8.6      "!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)";
     8.7 -be ([Transset_eclose RS Transset_univ, PowD] MRS 
     8.8 -    Transset_includes_summands RS conjE) 1;
     8.9 +by (etac ([Transset_eclose RS Transset_univ, PowD] MRS 
    8.10 +	  Transset_includes_summands RS conjE) 1);
    8.11  by (REPEAT (ares_tac [conjI,PowI] 1));
    8.12  val quniv_QPair_D = result();
    8.13