# 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.