src/HOL/NatDef.ML
changeset 2718 460fd0f8d478
parent 2680 20fa49e610ca
child 2891 d8f254ad1ab9
     1.1 --- a/src/HOL/NatDef.ML	Tue Mar 04 10:42:28 1997 +0100
     1.2 +++ b/src/HOL/NatDef.ML	Tue Mar 04 10:48:36 1997 +0100
     1.3 @@ -667,7 +667,7 @@
     1.4    | negate None = None;
     1.5  
     1.6  fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
     1.7 -  | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =
     1.8 +  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
     1.9        negate(decomp2(rel,T,lhs,rhs))
    1.10    | decomp _ = None
    1.11