| changeset 2268 | 79a2f085a7fd |
| parent 2164 | c87368fc736b |
| child 2441 | decc46a5cdb5 |
--- a/src/HOL/Nat.ML Thu Nov 28 10:50:43 1996 +0100 +++ b/src/HOL/Nat.ML Thu Nov 28 12:09:33 1996 +0100 @@ -639,6 +639,7 @@ end; fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j) + | negate None = None; fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs) | decomp(_$(Const("not",_)$(Const(rel,T)$lhs$rhs))) =