* HOL: alternative iff syntax;

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