# HG changeset patch
# User wenzelm
# Date 1584050711 -3600
# Node ID 317e9ebbc3e1ef90c8fb992ec4d488a9f97ea623
# Parent  e76692ec6e5a62c1f89b76be5722be277562bb78
updated for release;

diff -r e76692ec6e5a -r 317e9ebbc3e1 NEWS
--- a/NEWS	Thu Mar 12 21:25:53 2020 +0100
+++ b/NEWS	Thu Mar 12 23:05:11 2020 +0100
@@ -55,6 +55,13 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* Prover IDE startup is now much faster, because theory dependencies are
+no longer explored in advance. The overall session structure with its
+declarations of 'directories' is sufficient to locate theory files. Thus
+the "session focus" of option "isabelle jedit -S" has become obsolete
+(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
+sufficient and more convenient to start editing a particular session.
+
 * Actions isabelle.tooltip (CS+b) and isabelle.message (CS+m) display
 tooltip message popups, corresponding to mouse hovering with/without the
 CONTROL/COMMAND key pressed.
@@ -67,19 +74,16 @@
   isabelle.next-error (CS+n)
   isabelle.prev-error (CS+p)
 
-* Prover IDE startup is now much faster, because theory dependencies are
-no longer explored in advance. The overall session structure with its
-declarations of 'directories' is sufficient to locate theory files. Thus
-the "session focus" of option "isabelle jedit -S" has become obsolete
-(likewise for "isabelle vscode_server -S"). Existing option "-R" is both
-sufficient and more convenient to start editing a particular session.
-
 * Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax).
 
 * Action isabelle.jconsole (menu item Plugins / Isabelle / Java/VM
 Monitor) applies the jconsole tool on the running Isabelle/jEdit
 process. This allows to monitor resource usage etc.
 
+* More adequate default font sizes for Linux on HD / UHD displays:
+automatic font scaling is usually absent on Linux, in contrast to
+Windows and macOS.
+
 
 *** Isabelle/VSCode Prover IDE ***
 
@@ -89,12 +93,6 @@
 
 *** HOL ***
 
-* Removed multiplicativity assumption from normalization_semidom typeclass.
-  Introduced various new intermediate typeclasses with the multiplicativity
-  assumption; many theorem statements (especially involving GCD/LCM) had
-  to be adapted. This allows for a more natural instantiation of the 
-  algebraic typeclasses for e.g. Gaussian integers. INCOMPATIBILITY.
-
 * Improvements of the 'lift_bnf' command:
   - Add support for quotient types.
   - Generate transfer rules for the lifted map/set/rel/pred constants
@@ -109,6 +107,13 @@
 * ASCII membership syntax concerning big operators for infimum and
 supremum has been discontinued. INCOMPATIBILITY.
 
+* Removed multiplicativity assumption from class
+"normalization_semidom". Introduced various new intermediate classes
+with the multiplicativity assumption; many theorem statements
+(especially involving GCD/LCM) had to be adapted. This allows for a more
+natural instantiation of the algebraic typeclasses for e.g. Gaussian
+integers. INCOMPATIBILITY.
+
 * Clear distinction between types for bits (False / True) and Z2 (0 /
 1): theory HOL-Library.Bit has been renamed accordingly.
 INCOMPATIBILITY.