# HG changeset patch
# User paulson
# Date 938524347 -7200
# Node ID dcb93b29568303c75c36666c3b30a3834ffe8d68
# Parent  4074bc1e380d16cad65d9ebff01be9e7fa6b4ba6
zero_is_mult, by symmetry

diff -r 4074bc1e380d -r dcb93b295683 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Sep 28 14:24:22 1999 +0200
+++ b/src/HOL/Arith.ML	Tue Sep 28 15:12:27 1999 +0200
@@ -336,7 +336,13 @@
 by (induct_tac "n" 2);
 by (ALLGOALS Asm_simp_tac);
 qed "mult_is_0";
-Addsimps [mult_is_0];
+
+Goal "(0 = m*n) = (0=m | 0=n)";
+by (cut_facts_tac [mult_is_0] 1);
+by (full_simp_tac (simpset() addsimps [eq_commute]) 1);
+qed "zero_is_mult";
+
+Addsimps [mult_is_0, zero_is_mult];
 
 Goal "m <= m*(m::nat)";
 by (induct_tac "m" 1);