New one-point rules for quantifiers

--- 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