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