NEWS
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".