# HG changeset patch
# User paulson
# Date 932743668 -7200
# Node ID 5ba8d1e42ca6fd365413d5d45b89d828bf614e24
# Parent  e0730ffaafcc1505c35135554b4d4084c2ba78f7
zmult_ac are no longer included by default

diff -r e0730ffaafcc -r 5ba8d1e42ca6 src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Fri Jul 23 17:27:12 1999 +0200
+++ b/src/HOL/Integ/NatBin.ML	Fri Jul 23 17:27:48 1999 +0200
@@ -122,7 +122,8 @@
 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;
+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 (rtac (inj_int RS injD) 1);