* New bounded quantifier syntax (input only):
! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P

--- a/NEWS	Thu Mar 18 16:42:34 1999 +0100
+++ b/NEWS	Thu Mar 18 16:44:53 1999 +0100
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -71,6 +70,9 @@
 nat/int formulae where the two parts interact, such as `m < n ==>
 int(m) < int(n)'.
 
+* New bounded quantifier syntax (input only):
+  ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
+
 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
 -- avoids syntactic ambiguities and treats state, transition, and
 temporal levels more uniformly; introduces INCOMPATIBILITIES due to