# HG changeset patch
# User paulson
# Date 844676615 -7200
# Node ID bf3891343aa57ea093cee10dd99a78ae6e00108c
# Parent  6c0594bfa726c48653e3bf532ea992bea64dbf12
New one-point rules for quantifiers

diff -r 6c0594bfa726 -r bf3891343aa5 src/HOL/simpdata.ML
--- 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