# HG changeset patch
# User paulson
# Date 844762670 -7200
# Node ID b696f087f0520b697d89ad15aea81e735ea7e2bd
# Parent  5a5e508e2a2ba0547b6a4cef929946f0a2c737f3
Addition of one-point quantifier rewrite rules

diff -r 5a5e508e2a2b -r b696f087f052 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Mon Oct 07 10:55:51 1996 +0200
+++ b/src/FOL/simpdata.ML	Tue Oct 08 10:17:50 1996 +0200
@@ -138,7 +138,9 @@
 
 (*Miniscoping: pushing in existential quantifiers*)
 val ex_simps = map prove_fun 
-                ["(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
+                ["(EX x. x=t & P(x)) <-> P(t)",
+                 "(EX x. t=x & P(x)) <-> P(t)",
+                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
                  "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
                  "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
                  "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
@@ -147,7 +149,9 @@
 
 (*Miniscoping: pushing in universal quantifiers*)
 val all_simps = map prove_fun
-                ["(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
+                ["(ALL x. x=t --> P(x)) <-> P(t)",
+                 "(ALL x. t=x --> P(x)) <-> P(t)",
+                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
                  "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
                  "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
                  "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",