--- 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))",