Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Missing case in instantiation of Transitivity prover (negate(None)=None)
authornipkow
Thu, 28 Nov 1996 12:09:33 +0100
changeset 2268 79a2f085a7fd
parent 2267 b2326aefecbc
child 2269 820f68aec6ee
Missing case in instantiation of Transitivity prover (negate(None)=None)
src/HOL/Nat.ML file | annotate | diff | comparison | revisions 
--- 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))) =
isabelle