changeset 14378 | 69c4d5997669 |
parent 14124 | 883c38e2d4c0 |
child 14398 | c5c47703f763 |
--- a/src/HOL/ex/BinEx.thy Thu Feb 05 10:45:28 2004 +0100 +++ b/src/HOL/ex/BinEx.thy Tue Feb 10 12:02:11 2004 +0100 @@ -470,7 +470,7 @@ apply assumption apply (simp add: normal_Pls_eq_0) apply (simp only: number_of_minus zminus_0 iszero_def - zminus_equation [of _ "0"]) + minus_equation_iff [of _ "0"]) apply (simp add: eq_commute) done