# HG changeset patch
# User paulson
# Date 842259572 -7200
# Node ID d33a5d59a29ad245ee50c8b29e9a3cb4588d13e2
# Parent  ae390b599213f34362f6248a5d9aa81f7925bf29
Removal of (EX x. P) <-> P and (ALL x. P) <-> P
from ex_simps and all_simps. as they are already in quant_simps.

diff -r ae390b599213 -r d33a5d59a29a src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Sep 06 11:56:12 1996 +0200
+++ b/src/FOL/simpdata.ML	Mon Sep 09 10:59:32 1996 +0200
@@ -138,8 +138,7 @@
 
 (*Miniscoping: pushing in existential quantifiers*)
 val ex_simps = map prove_fun 
-                ["(EX x. P) <-> P",
-                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
+                ["(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))",
@@ -148,8 +147,7 @@
 
 (*Miniscoping: pushing in universal quantifiers*)
 val all_simps = map prove_fun
-                ["(ALL x. P) <-> P",
-                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
+                ["(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))",