# 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'))"