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