# HG changeset patch
# User paulson
# Date 963485966 -7200
# Node ID de04717eed7855bf60c47a35f198621bd9253dba
# Parent  ee5c9672d20831d917b276dffa9ff9747756c08e
removed needless premises

diff -r ee5c9672d208 -r de04717eed78 src/ZF/Arith.ML
--- 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);