--- a/src/HOL/arith_data.ML Fri Sep 04 13:24:10 1998 +0200
+++ b/src/HOL/arith_data.ML Mon Sep 07 10:40:17 1998 +0200
@@ -222,13 +222,13 @@
(*This proof requires natdiff_cancel_sums*)
-goal Arith.thy "!!n::nat. m<n --> m<l --> (l-n) < (l-m)";
+Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)";
by (induct_tac "l" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (etac less_SucE 1);
+by (Clarify_tac 2);
+by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
Suc_diff_le]) 1);
-by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
qed_spec_mp "diff_less_mono2";