expandshort
authorpaulson
Fri Jan 29 17:08:20 1999 +0100 (1999-01-29)
changeset 6163be8234f37e48
parent 6162 484adda70b65
child 6164 a0e9501d56f8
expandshort
src/ZF/Arith.ML
src/ZF/Epsilon.ML
src/ZF/ex/Limit.ML
src/ZF/ex/Primrec.ML
src/ZF/upair.ML
     1.1 --- a/src/ZF/Arith.ML	Fri Jan 29 16:26:12 1999 +0100
     1.2 +++ b/src/ZF/Arith.ML	Fri Jan 29 17:08:20 1999 +0100
     1.3 @@ -535,7 +535,7 @@
     1.4  
     1.5  Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
     1.6  by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
     1.7 -be rev_mp 1;
     1.8 +by (etac rev_mp 1);
     1.9  by (induct_tac "n" 1);
    1.10  by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
    1.11  by (blast_tac (claset() addSEs [leE] 
     2.1 --- a/src/ZF/Epsilon.ML	Fri Jan 29 16:26:12 1999 +0100
     2.2 +++ b/src/ZF/Epsilon.ML	Fri Jan 29 17:08:20 1999 +0100
     2.3 @@ -217,8 +217,8 @@
     2.4  Goal "rank(Pow(a)) = succ(rank(a))";
     2.5  by (rtac (rank RS trans) 1);
     2.6  by (rtac le_anti_sym 1);
     2.7 -br UN_upper_le 2;
     2.8 -br UN_least_le 1;
     2.9 +by (rtac UN_upper_le 2);
    2.10 +by (rtac UN_least_le 1);
    2.11  by (auto_tac (claset() addIs [rank_mono], simpset()));
    2.12  qed "rank_Pow";
    2.13  
     3.1 --- a/src/ZF/ex/Limit.ML	Fri Jan 29 16:26:12 1999 +0100
     3.2 +++ b/src/ZF/ex/Limit.ML	Fri Jan 29 17:08:20 1999 +0100
     3.3 @@ -1425,7 +1425,7 @@
     3.4  
     3.5  Goal "emb_chain(DD,ee) ==> cpo(Dinf(DD,ee))";
     3.6  by (rtac subcpo_cpo 1);
     3.7 -be subcpo_Dinf 1;
     3.8 +by (etac subcpo_Dinf 1);
     3.9  by (auto_tac (claset() addIs [cpo_iprod, emb_chain_cpo], simpset()));
    3.10  qed "cpo_Dinf";
    3.11  
     4.1 --- a/src/ZF/ex/Primrec.ML	Fri Jan 29 16:26:12 1999 +0100
     4.2 +++ b/src/ZF/ex/Primrec.ML	Fri Jan 29 17:08:20 1999 +0100
     4.3 @@ -159,7 +159,7 @@
     4.4  \             i#+j < ack(succ(succ(succ(succ(k)))), j)";
     4.5  by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
     4.6  by (rtac (ack_add_bound RS lt_trans2) 2);
     4.7 -br add_lt_mono 1;
     4.8 +by (rtac add_lt_mono 1);
     4.9  by Auto_tac;
    4.10  qed "ack_add_bound2";
    4.11  
     5.1 --- a/src/ZF/upair.ML	Fri Jan 29 16:26:12 1999 +0100
     5.2 +++ b/src/ZF/upair.ML	Fri Jan 29 17:08:20 1999 +0100
     5.3 @@ -230,8 +230,8 @@
     5.4  by (rtac theI 1);
     5.5  by (rtac classical 1);
     5.6  by (resolve_tac prems 1);
     5.7 -be (the_0 RS subst) 1;
     5.8 -ba 1;
     5.9 +by (etac (the_0 RS subst) 1);
    5.10 +by (assume_tac 1);
    5.11  qed "theI2";
    5.12  
    5.13  (*** if -- a conditional expression for formulae ***)