diff -r 0d7628966069 -r eacebbcafe57 src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Wed Jun 14 17:45:01 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Wed Jun 14 17:46:10 2000 +0200
@@ -126,14 +126,10 @@
 
 Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
 by (case_tac "#0 <= z'" 1);
-by (subgoal_tac "z'*z <= #0" 2);
-by (rtac (neg_imp_zmult_nonpos_iff RS iffD2) 3);
-by (auto_tac (claset(),
-	      simpset() addsimps [zmult_commute]));
-by (subgoal_tac "#0 <= z*z'" 1);
-by (force_tac (claset() addDs [zmult_zle_mono1], simpset()) 2);
+by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
 by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
+				      int_0_le_mult_iff]) 1);
 qed "nat_mult_distrib";
 
 Goal "(number_of v :: nat) * number_of v' = \