# HG changeset patch
# User wenzelm
# Date 1130414346 -7200
# Node ID 71f250e05e057458c19dce518e922a257df8f3c5
# Parent  8b9c6af78a675f4e0537e1db95b48952d69c37e7
* HOL: alternative iff syntax;

diff -r 8b9c6af78a67 -r 71f250e05e05 NEWS
--- 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".