# HG changeset patch
# User nipkow
# Date 786805947 -3600
# Node ID 663cead79989dbca770304f661db30f8041ef628
# Parent  2757544bbe6ddb54a8e31fd3999d83ced96cfadf
Added (? x. x=t & P) = P to the simpset.

diff -r 2757544bbe6d -r 663cead79989 simpdata.ML
--- a/simpdata.ML	Wed Dec 07 14:11:22 1994 +0100
+++ b/simpdata.ML	Wed Dec 07 14:12:27 1994 +0100
@@ -59,7 +59,7 @@
    "(P & False) = False", "(False & P) = False", "(P & P) = P",
    "(P | True) = True", "(True | P) = True", 
    "(P | False) = P", "(False | P) = P", "(P | P) = P",
-   "(!x.P) = P", "(? x.P) = P",
+   "(!x.P) = P", "(? x.P) = P", "(? x. x=t & P) = P",
    "(P|Q --> R) = ((P-->R)&(Q-->R))" ];
 
 in