* New bounded quantifier syntax (input only):
authornipkow
Thu Mar 18 16:44:53 1999 +0100 (1999-03-18)
changeset 640386e9d24f4238
parent 6402 2b23e14dd386
child 6404 2daaf2943c79
* New bounded quantifier syntax (input only):
! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
NEWS
     1.1 --- a/NEWS	Thu Mar 18 16:42:34 1999 +0100
     1.2 +++ b/NEWS	Thu Mar 18 16:44:53 1999 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -71,6 +70,9 @@
     1.9  nat/int formulae where the two parts interact, such as `m < n ==>
    1.10  int(m) < int(n)'.
    1.11  
    1.12 +* New bounded quantifier syntax (input only):
    1.13 +  ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P
    1.14 +
    1.15  * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
    1.16  -- avoids syntactic ambiguities and treats state, transition, and
    1.17  temporal levels more uniformly; introduces INCOMPATIBILITIES due to