--- a/src/HOL/Divides.ML Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/Divides.ML Sat Jan 09 15:24:11 1999 +0100
@@ -189,14 +189,13 @@
(* Antimonotonicity of div in second argument *)
Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
by (subgoal_tac "0<n" 1);
- by (Simp_tac 2);
+ by (Asm_simp_tac 2);
by (res_inst_tac [("n","k")] less_induct 1);
-by (Simp_tac 1);
by (rename_tac "k" 1);
by (case_tac "k<n" 1);
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
by (subgoal_tac "~(k<m)" 1);
- by (Simp_tac 2);
+ by (Asm_simp_tac 2);
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
@@ -209,19 +208,18 @@
by (subgoal_tac "m div n <= m div 1" 1);
by (Asm_full_simp_tac 1);
by (rtac div_le_mono2 1);
-by (ALLGOALS Simp_tac);
+by (ALLGOALS Asm_simp_tac);
qed "div_le_dividend";
Addsimps [div_le_dividend];
(* Similar for "less than" *)
Goal "1<n ==> (0 < m) --> (m div n < m)";
by (res_inst_tac [("n","m")] less_induct 1);
-by (Simp_tac 1);
by (rename_tac "m" 1);
by (case_tac "m<n" 1);
by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
by (subgoal_tac "0<n" 1);
- by (Simp_tac 2);
+ by (Asm_simp_tac 2);
by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
by (case_tac "n<m" 1);
by (subgoal_tac "(m-n) div n < (m-n)" 1);
@@ -230,7 +228,7 @@
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
(* case n=m *)
by (subgoal_tac "m=n" 1);
- by (Simp_tac 2);
+ by (Asm_simp_tac 2);
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
qed_spec_mp "div_less_dividend";
Addsimps [div_less_dividend];