# HG changeset patch
# User paulson
# Date 938525514 -7200
# Node ID 94b2a50e69a5870cba563cd09caad96610c4c7a7
# Parent  9024e9d370c72983f601cd3903be0d3767141f02
zero_is_mult, by symmetry

diff -r 9024e9d370c7 -r 94b2a50e69a5 src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Tue Sep 28 15:30:52 1999 +0200
+++ b/src/HOL/Integ/NatBin.ML	Tue Sep 28 15:31:54 1999 +0200
@@ -309,7 +309,7 @@
 	  [diff_0_eq_0, add_0, add_0_right, add_pred, 
 	   diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
 	   mult_0, mult_0_right, mult_1, mult_1_right, 
-	   mult_is_0, zero_less_mult_iff,
+	   mult_is_0, zero_is_mult, zero_less_mult_iff,
 	   mult_eq_1_iff]);
 
 AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);