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.
Deleted comment.
authornipkow
Thu, 24 Jul 1997 11:20:12 +0200
changeset 3573 7544c866315c
parent 3572 5ec1589eac1b
child 3574 5995ab73d790
Deleted comment.
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/simpdata.ML	Thu Jul 24 11:13:12 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu Jul 24 11:20:12 1997 +0200
@@ -103,7 +103,7 @@
    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    "((~P) = (~Q)) = (P=Q)",
    "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
-   "(? x. x=t & P(x)) = P(t)", (*"(? x. t=x & P(x)) = P(t)",*)
+   "(? x. x=t & P(x)) = P(t)",
    "(! x. t=x --> P(x)) = P(t)" ];
 
 (*Add congruence rules for = (instead of ==) *)
isabelle