Misc modifs such as expandshort
authorlcp
Thu Nov 18 14:57:05 1993 +0100 (1993-11-18)
changeset 127eec6bb9c58ea
parent 126 0b0055b3ccfe
child 128 b0ec0c1bddb7
Misc modifs such as expandshort
src/ZF/Arith.ML
src/ZF/arith.ML
     1.1 --- a/src/ZF/Arith.ML	Tue Nov 16 19:50:20 1993 +0100
     1.2 +++ b/src/ZF/Arith.ML	Thu Nov 18 14:57:05 1993 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4  (*Addition is the inverse of subtraction*)
     1.5  goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
     1.6  by (forward_tac [lt_nat_in_nat] 1);
     1.7 -be nat_succI 1;
     1.8 +by (etac nat_succI 1);
     1.9  by (etac rev_mp 1);
    1.10  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.11  by (ALLGOALS (asm_simp_tac arith_ss));
    1.12 @@ -334,7 +334,7 @@
    1.13  (*strict, in 1st argument*)
    1.14  goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
    1.15  by (forward_tac [lt_nat_in_nat] 1);
    1.16 -ba 1;
    1.17 +by (assume_tac 1);
    1.18  by (etac succ_lt_induct 1);
    1.19  by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
    1.20  val add_lt_mono1 = result();
     2.1 --- a/src/ZF/arith.ML	Tue Nov 16 19:50:20 1993 +0100
     2.2 +++ b/src/ZF/arith.ML	Thu Nov 18 14:57:05 1993 +0100
     2.3 @@ -228,7 +228,7 @@
     2.4  (*Addition is the inverse of subtraction*)
     2.5  goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
     2.6  by (forward_tac [lt_nat_in_nat] 1);
     2.7 -be nat_succI 1;
     2.8 +by (etac nat_succI 1);
     2.9  by (etac rev_mp 1);
    2.10  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.11  by (ALLGOALS (asm_simp_tac arith_ss));
    2.12 @@ -334,7 +334,7 @@
    2.13  (*strict, in 1st argument*)
    2.14  goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
    2.15  by (forward_tac [lt_nat_in_nat] 1);
    2.16 -ba 1;
    2.17 +by (assume_tac 1);
    2.18  by (etac succ_lt_induct 1);
    2.19  by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
    2.20  val add_lt_mono1 = result();