# HG changeset patch
# User lcp
# Date 753631025 -3600
# Node ID eec6bb9c58eada95bcfca052859a434a1b54b213
# Parent  0b0055b3ccfedb74f41fac20982b6f022bf033aa
Misc modifs such as expandshort

diff -r 0b0055b3ccfe -r eec6bb9c58ea src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Tue Nov 16 19:50:20 1993 +0100
+++ b/src/ZF/Arith.ML	Thu Nov 18 14:57:05 1993 +0100
@@ -228,7 +228,7 @@
 (*Addition is the inverse of subtraction*)
 goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
 by (forward_tac [lt_nat_in_nat] 1);
-be nat_succI 1;
+by (etac nat_succI 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS (asm_simp_tac arith_ss));
@@ -334,7 +334,7 @@
 (*strict, in 1st argument*)
 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
 by (forward_tac [lt_nat_in_nat] 1);
-ba 1;
+by (assume_tac 1);
 by (etac succ_lt_induct 1);
 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
 val add_lt_mono1 = result();
diff -r 0b0055b3ccfe -r eec6bb9c58ea src/ZF/arith.ML
--- a/src/ZF/arith.ML	Tue Nov 16 19:50:20 1993 +0100
+++ b/src/ZF/arith.ML	Thu Nov 18 14:57:05 1993 +0100
@@ -228,7 +228,7 @@
 (*Addition is the inverse of subtraction*)
 goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
 by (forward_tac [lt_nat_in_nat] 1);
-be nat_succI 1;
+by (etac nat_succI 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS (asm_simp_tac arith_ss));
@@ -334,7 +334,7 @@
 (*strict, in 1st argument*)
 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
 by (forward_tac [lt_nat_in_nat] 1);
-ba 1;
+by (assume_tac 1);
 by (etac succ_lt_induct 1);
 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
 val add_lt_mono1 = result();