# HG changeset patch # User paulson # Date 903515162 -7200 # Node ID ea33e66dceddf9f66c81d5f3a83fe1601cf8b3e5 # Parent cd53e59688a82ba1a4e67ce022975964eaffc71b Some new theorems. zero_less_diff replaces less_imp_diff_positive diff -r cd53e59688a8 -r ea33e66dcedd src/HOL/Arith.ML --- a/src/HOL/Arith.ML Tue Aug 18 10:27:14 1998 +0200 +++ b/src/HOL/Arith.ML Wed Aug 19 10:26:02 1998 +0200 @@ -375,7 +375,7 @@ by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1); qed "diff_Suc_less_diff"; -Goal "!!n::nat. m - n <= Suc m - n"; +Goal "m - n <= Suc m - n"; by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); by (ALLGOALS Asm_simp_tac); qed "diff_le_Suc_diff"; @@ -429,20 +429,20 @@ by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); qed_spec_mp "diffs0_imp_equal"; -Goal "m 0 ? k. 0 ? k. 0