NEWS
changeset 68796 9ca183045102
parent 68770 add44e2b8cb0
child 68803 169bf32b35dd
     1.1 --- a/NEWS	Thu Aug 23 17:09:37 2018 +0000
     1.2 +++ b/NEWS	Thu Aug 23 17:09:39 2018 +0000
     1.3 @@ -14,6 +14,15 @@
     1.4  specified in seconds; a negative value means it is disabled (default).
     1.5  
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Simplified syntax setup for big operators under image. In rare
    1.10 +situations, type conversions are not inserted implicitly any longer
    1.11 +and need to be given explicitly. Auxiliary abbreviations INFIMUM,
    1.12 +SUPREMUM, UNION, INTER should now rarely occur in output and are just
    1.13 +retained as migration auxiliary. INCOMPATIBILITY.
    1.14 +
    1.15 +
    1.16  New in Isabelle2018 (August 2018)
    1.17  ---------------------------------
    1.18