Missing case in instantiation of Transitivity prover (negate(None)=None)
authornipkow
Thu Nov 28 12:09:33 1996 +0100 (1996-11-28)
changeset 226879a2f085a7fd
parent 2267 b2326aefecbc
child 2269 820f68aec6ee
Missing case in instantiation of Transitivity prover (negate(None)=None)
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Thu Nov 28 10:50:43 1996 +0100
     1.2 +++ b/src/HOL/Nat.ML	Thu Nov 28 12:09:33 1996 +0100
     1.3 @@ -639,6 +639,7 @@
     1.4    end;
     1.5  
     1.6  fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
     1.7 +  | negate None = None;
     1.8  
     1.9  fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
    1.10    | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =