Mercurial Mercurial > repos > Old_HOL / 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.
Added (? x. x=t & P) = P to the simpset.
authornipkow
Wed, 07 Dec 1994 14:12:27 +0100
changeset 198 663cead79989
parent 197 2757544bbe6d
child 199 ad45e477926c
Added (? x. x=t & P) = P to the simpset.
simpdata.ML file | annotate | diff | comparison | revisions 
--- a/simpdata.ML	Wed Dec 07 14:11:22 1994 +0100
+++ b/simpdata.ML	Wed Dec 07 14:12:27 1994 +0100
@@ -59,7 +59,7 @@
    "(P & False) = False", "(False & P) = False", "(P & P) = P",
    "(P | True) = True", "(True | P) = True", 
    "(P | False) = P", "(False | P) = P", "(P | P) = P",
-   "(!x.P) = P", "(? x.P) = P",
+   "(!x.P) = P", "(? x.P) = P", "(? x. x=t & P) = P",
    "(P|Q --> R) = ((P-->R)&(Q-->R))" ];
 
 in
Old_HOL