# HG changeset patch
# User paulson
# Date 960997483 -7200
# Node ID 7b34ffecaaa80504c67b01f6be8f392f14366039
# Parent  144b06e6729ee4f4709a88f8cd567a64f51e6ca6
new default simprules for m*n = 0

diff -r 144b06e6729e -r 7b34ffecaaa8 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Tue Jun 13 18:36:06 2000 +0200
+++ b/src/HOL/Integ/Bin.ML	Wed Jun 14 17:44:43 2000 +0200
@@ -270,6 +270,13 @@
 by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1);
 qed "zmult_eq_0_iff";
 
+Goal "((#0::int) = m*n) = (#0 = m | #0 = n)";
+by (stac eq_commute 1 THEN stac zmult_eq_0_iff 1);
+by Auto_tac;
+qed "zmult_0_eq_iff";
+
+Addsimps [zmult_eq_0_iff, zmult_0_eq_iff];
+
 Goal "(w < z + (#1::int)) = (w<z | w=z)";
 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
 qed "zless_add1_eq";