Added (? x. t=x) = True
authornipkow
Fri Oct 25 15:02:09 1996 +0200 (1996-10-25)
changeset 21292ffe6e24f38d
parent 2128 4e8644805af2
child 2130 53b6e0bc8ccf
Added (? x. t=x) = True
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Oct 24 11:41:43 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Oct 25 15:02:09 1996 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4     "(P | True) = True", "(True | P) = True", 
     1.5     "(P | False) = P", "(False | P) = P", "(P | P) = P",
     1.6     "((~P) = (~Q)) = (P=Q)",
     1.7 -   "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
     1.8 +   "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
     1.9     "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
    1.10     "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
    1.11