author | paulson |
Thu, 13 Jul 2000 12:59:26 +0200 | |
changeset 9301 | de04717eed78 |
parent 9300 | ee5c9672d208 |
child 9302 | 8adf653d40a1 |
src/ZF/Arith.ML | file | annotate | diff | comparison | revisions |
--- a/src/ZF/Arith.ML Thu Jul 13 12:56:42 2000 +0200 +++ b/src/ZF/Arith.ML Thu Jul 13 12:59:26 2000 +0200 @@ -521,9 +521,9 @@ qed "mult_eq_self_implies_10"; (*Thanks to Sten Agerholm*) -Goal "[|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k"; +Goal "[|k#+m le k#+n; k:nat |] ==> m le n"; by (etac rev_mp 1); -by (induct_tac "m" 1); +by (induct_tac "k" 1); by (Asm_simp_tac 1); by Safe_tac; by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt]) 1);