# HG changeset patch
# User paulson
# Date 843494993 -7200
# Node ID 968f78b525400d08e442d6ab7d54cb78e81b750f
# Parent  72754e060aa28d9cb32a872893fc271278fbe027
Proof of mult_le_mono is now more robust

diff -r 72754e060aa2 -r 968f78b52540 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Sep 23 17:47:49 1996 +0200
+++ b/src/HOL/Arith.ML	Mon Sep 23 18:09:53 1996 +0200
@@ -530,9 +530,11 @@
 
 (*<=monotonicity, BOTH arguments*)
 goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l";
+by (etac (mult_le_mono1 RS le_trans) 1);
 by (rtac le_trans 1);
-by (ALLGOALS 
-    (deepen_tac (!claset addIs [mult_commute RS ssubst, mult_le_mono1]) 0));
+by (stac mult_commute 2);
+by (etac mult_le_mono1 2);
+by (simp_tac (!simpset addsimps [mult_commute]) 1);
 qed "mult_le_mono";
 
 (*strict, in 1st argument; proof is by induction on k>0*)