changeset 17996 | 71f250e05e05 |
parent 17991 | ca0958ab3293 |
child 18020 | d23a846598d2 |
--- a/NEWS Thu Oct 27 13:54:43 2005 +0200 +++ b/NEWS Thu Oct 27 13:59:06 2005 +0200 @@ -57,6 +57,10 @@ *** HOL *** +* Alternative iff syntax "A <-> B" for equality on bool (with priority +25 like -->); output depends on the "iff" print_mode, the default is +"A = B" (with priority 50). + * In the context of the assumption "~(s = t)" the Simplifier rewrites "t = s" to False (by simproc "neq_simproc"). For backward compatibility this can be disabled by ML "reset use_neq_simproc".