New one-point rules for quantifiers
authorpaulson
Mon Oct 07 10:23:35 1996 +0200 (1996-10-07)
changeset 2054bf3891343aa5
parent 2053 6c0594bfa726
child 2055 cc274e47f607
New one-point rules for quantifiers
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Tue Oct 01 18:19:12 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Mon Oct 07 10:23:35 1996 +0200
     1.3 @@ -120,7 +120,8 @@
     1.4       "(P | False) = P", "(False | P) = P", "(P | P) = P",
     1.5       "((~P) = (~Q)) = (P=Q)",
     1.6       "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
     1.7 -     "(? x. x=t & P(x)) = P(t)", "(! x. x=t --> P(x)) = P(t)" ];
     1.8 +     "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
     1.9 +     "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
    1.10  
    1.11  in
    1.12