zero_is_mult, by symmetry
authorpaulson
Tue, 28 Sep 1999 15:31:54 +0200
changeset 7625 94b2a50e69a5
parent 7624 9024e9d370c7
child 7626 5997f35954d7
zero_is_mult, by symmetry
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]);