# HG changeset patch
# User wenzelm
# Date 1738608793 -3600
# Node ID 4df95adf6b66efe039e91e8ef1b1986dc07819f5
# Parent  d526ae8fc0a0ef67917a5992ceb7bb831c50b44b
tuned;

diff -r d526ae8fc0a0 -r 4df95adf6b66 NEWS
--- a/NEWS	Mon Feb 03 19:50:27 2025 +0100
+++ b/NEWS	Mon Feb 03 19:53:13 2025 +0100
@@ -156,7 +156,6 @@
 'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac".
 
 
-
 *** Isabelle/jEdit Prover IDE ***
 
 * Action isabelle.select_structure (with keyboard shortcut C+7) extends
@@ -249,7 +248,6 @@
   \renewcommand{\isakeywordTHREE}[1]{\isakeyword{\color[RGB]{0,153,255}#1}}
 
 
-
 *** HOL ***
 
 * Sledgehammer:
@@ -432,7 +430,8 @@
 remains for formal names (files, DNS etc.).
 
 * Update of the MLton SML compiler to work better with current macOS
-versions (including ARM). Windows and Linux ARM remain unsupported.
+versions (including ARM): this requires a C compiler and libgmp. Windows
+and Linux ARM remain unsupported, as before.