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.
new theorem
authorpaulson
Tue, 15 Jan 2002 15:07:41 +0100
changeset 12765 fb3f9887d0b7
parent 12764 b43333dc6e7d
child 12766 7d67b065925e
new theorem
src/FOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/simpdata.ML	Tue Jan 15 13:14:39 2002 +0100
+++ b/src/FOL/simpdata.ML	Tue Jan 15 15:07:41 2002 +0100
@@ -203,6 +203,7 @@
 int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
 prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
 
+prove     "not_imp" "~(P --> Q) <-> (P & ~Q)";
 prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
 
 prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
isabelle