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