Added P&P&Q = P&Q and P|P|Q = P|Q.
authornipkow
Tue Mar 18 08:42:18 1997 +0100 (1997-03-18)
changeset 28009741c4c6b62b
parent 2799 1857b7e2e095
child 2801 56948cb1a1f9
Added P&P&Q = P&Q and P|P|Q = P|Q.
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Mon Mar 17 15:38:26 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Tue Mar 18 08:42:18 1997 +0100
     1.3 @@ -96,9 +96,11 @@
     1.4     "(P --> True) = True", "(P --> P) = True",
     1.5     "(P --> False) = (~P)", "(P --> ~P) = (~P)",
     1.6     "(P & True) = P", "(True & P) = P", 
     1.7 -   "(P & False) = False", "(False & P) = False", "(P & P) = P",
     1.8 +   "(P & False) = False", "(False & P) = False",
     1.9 +   "(P & P) = P", "(P & (P & Q)) = (P & Q)",
    1.10     "(P | True) = True", "(True | P) = True", 
    1.11 -   "(P | False) = P", "(False | P) = P", "(P | P) = P",
    1.12 +   "(P | False) = P", "(False | P) = P",
    1.13 +   "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    1.14     "((~P) = (~Q)) = (P=Q)",
    1.15     "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
    1.16     "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",