# HG changeset patch
# User wenzelm
# Date 1163069931 -3600
# Node ID b8db43faaf9ee840474dbd8388312dfb75673668
# Parent  14d4e7f78e463012aa62a56a8a2cc62c27dfbedb
HOL: less/less_eq on bool, modified syntax;

diff -r 14d4e7f78e46 -r b8db43faaf9e NEWS
--- a/NEWS	Thu Nov 09 11:58:50 2006 +0100
+++ b/NEWS	Thu Nov 09 11:58:51 2006 +0100
@@ -583,6 +583,10 @@
 This in general only affects hand-written proof tactics, simprocs and so on.
 INCOMPATIBILITY: grep your sourcecode and replace names.
 
+* Relations less (<) and less_eq (<=) are also available on type bool.
+Modified syntax to disallow nesting without explicit parentheses,
+e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z".
+
 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
 
 * Relation composition operator "op O" now has precedence 75 and binds