src/FOL/simpdata.ML
changeset 13149 773657d466cb
parent 12825 f1f7964ed05c
child 13462 56610e2ba220
--- a/src/FOL/simpdata.ML	Tue May 14 12:33:42 2002 +0200
+++ b/src/FOL/simpdata.ML	Wed May 15 10:42:32 2002 +0200
@@ -57,6 +57,7 @@
   "(ALL x. x=t --> P(x)) <-> P(t)",
   "(ALL x. t=x --> P(x)) <-> P(t)",
   "(EX x. P) <-> P",
+  "EX x. x=t", "EX x. t=x",
   "(EX x. x=t & P(x)) <-> P(t)",
   "(EX x. t=x & P(x)) <-> P(t)"]);