# HG changeset patch
# User nipkow
# Date 791384537 -3600
# Node ID 21c405b4039fd1caebba322c867a832d71f7eb6c
# Parent  d465d3be274424c6e604a9b11bae0a1c7ca1cc74
Added some simplifications for ? x.

diff -r d465d3be2744 -r 21c405b4039f simpdata.ML
--- a/simpdata.ML	Thu Jan 26 10:41:21 1995 +0100
+++ b/simpdata.ML	Sun Jan 29 14:02:17 1995 +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. x=t & P) = P",
+   "(!x.P) = P", "(? x.P) = P", "? x. x=t", "(? x. x=t & P(x)) = P(t)",
    "(P|Q --> R) = ((P-->R)&(Q-->R))" ];
 
 in
@@ -124,7 +124,8 @@
         (fn prems => [REPEAT(resolve_tac prems 1)])
   in equal_intr lemma1 lemma2 end;
 
-(** '&' congruence rule: not included by default! *)
+(* '&' congruence rule: not included by default!
+   May slow rewrite proofs down by as much as 50% *)
 
 val conj_cong = impI RSN
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"