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