# HG changeset patch # User wenzelm # Date 1565720355 -7200 # Node ID 7783bece74b440b4b19851150b878d4325dda640 # Parent 1182ea5c9a6e15adca84e9fd270829b77a42945b tuned whitespace; diff -r 1182ea5c9a6e -r 7783bece74b4 NEWS --- a/NEWS Tue Aug 13 20:17:02 2019 +0200 +++ b/NEWS Tue Aug 13 20:19:15 2019 +0200 @@ -1,5 +1,3 @@ - - Isabelle NEWS -- history of user-relevant changes ================================================= @@ -20,20 +18,21 @@ *** HOL *** -* ASCII membership syntax concerning big operators for infimum -and supremum is gone. INCOMPATIBILITY. - -* Clear distinction between types for bits (False / True) and -Z2 (0 / 1): theory HOL/Library/Bit.thy has been renamed accordingly. -INCOMPATIBILITY. - -* Fact collection sign_simps contains only simplification rules -for products being less / greater / equal to zero; combine with -existing collections algebra_simps or field_simps to obtain -reasonable simplification. INCOMPATIBILITY. - -* Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) associates -to the left now as is customary. +* ASCII membership syntax concerning big operators for infimum and +supremum is gone. INCOMPATIBILITY. + +* Clear distinction between types for bits (False / True) and Z2 (0 / +1): theory HOL/Library/Bit.thy has been renamed accordingly. +INCOMPATIBILITY. + +* Fact collection sign_simps contains only simplification rules for +products being less / greater / equal to zero; combine with existing +collections algebra_simps or field_simps to obtain reasonable +simplification. INCOMPATIBILITY. + +* Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) +associates to the left now as is customary. + New in Isabelle2019 (June 2019)