NEWS
changeset 70524 7783bece74b4
parent 70522 f2d58cafbc13
child 70525 1615b6808192
--- 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)