--- a/src/HOL/Divides.ML Thu Aug 13 18:07:56 1998 +0200
+++ b/src/HOL/Divides.ML Thu Aug 13 18:14:26 1998 +0200
@@ -10,7 +10,7 @@
(** Less-then properties **)
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
+Goal "[| 0<n; ~ m<n |] ==> m - n < m";
by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
by (Blast_tac 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
@@ -200,9 +200,10 @@
by (trans_tac 2);
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
- by (best_tac (claset() addIs [le_trans]
- addss (simpset() addsimps [diff_less])) 1);
-by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 1));
+by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
+br le_trans 1;
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
qed "div_le_mono2";
Goal "0<n ==> m div n <= m";