# HG changeset patch # User nipkow # Date 846248529 -7200 # Node ID 2ffe6e24f38d53df72695a7b80ff1d3941421d98 # Parent 4e8644805af22a479235136c5b1d22a8263160fe Added (? x. t=x) = True diff -r 4e8644805af2 -r 2ffe6e24f38d src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Thu Oct 24 11:41:43 1996 +0200 +++ b/src/HOL/simpdata.ML Fri Oct 25 15:02:09 1996 +0200 @@ -121,7 +121,7 @@ "(P | True) = True", "(True | P) = True", "(P | False) = P", "(False | P) = P", "(P | P) = P", "((~P) = (~Q)) = (P=Q)", - "(!x.P) = P", "(? x.P) = P", "? x. x=t", + "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];