Deleted comment.
authornipkow
Thu Jul 24 11:20:12 1997 +0200 (1997-07-24)
changeset 35737544c866315c
parent 3572 5ec1589eac1b
child 3574 5995ab73d790
Deleted comment.
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Jul 24 11:13:12 1997 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu Jul 24 11:20:12 1997 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4     "(P | P) = P", "(P | (P | Q)) = (P | Q)",
     1.5     "((~P) = (~Q)) = (P=Q)",
     1.6     "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
     1.7 -   "(? x. x=t & P(x)) = P(t)", (*"(? x. t=x & P(x)) = P(t)",*)
     1.8 +   "(? x. x=t & P(x)) = P(t)",
     1.9     "(! x. t=x --> P(x)) = P(t)" ];
    1.10  
    1.11  (*Add congruence rules for = (instead of ==) *)