Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/simpdata.ML
changeset 2054 bf3891343aa5
parent 2036 62ff902eeffc
child 2082 8659e3063a30 
--- a/src/HOL/simpdata.ML	Tue Oct 01 18:19:12 1996 +0200
+++ b/src/HOL/simpdata.ML	Mon Oct 07 10:23:35 1996 +0200
@@ -120,7 +120,8 @@
      "(P | False) = P", "(False | P) = P", "(P | P) = P",
      "((~P) = (~Q)) = (P=Q)",
      "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
-     "(? x. x=t & P(x)) = P(t)", "(! x. x=t --> P(x)) = P(t)" ];
+     "(? 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)" ];
 
 in
isabelle