# HG changeset patch
# User nipkow
# Date 921771893 -3600
# Node ID 86e9d24f4238b3db869d7e7e9d6d1274f7b15c38
# Parent  2b23e14dd386fec1e5c7a140edd3449b8c5ef525
* New bounded quantifier syntax (input only):
  ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P

diff -r 2b23e14dd386 -r 86e9d24f4238 NEWS
--- 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