--- a/NEWS Wed Oct 16 21:41:05 2024 +0200
+++ b/NEWS Wed Oct 16 22:07:04 2024 +0200
@@ -47,12 +47,13 @@
Pure, and "\<forall>x\<in>A. B x" or "\<exists>x\<in>A. B x" in HOL.
* Inner syntax printing now supports type constraints for constants:
-this is guarded by the configuration option "show_consts_markup". Ast
-translation rules (command 'translations') and mixfix notation work with
-or without such extra constraints, but ML translation functions (command
-'print_ast_translation') need may need to be changed slightly. Rare
-INCOMPATIBILITY. The Prover IDE displays type constraints for constants
-as for variables, e.g. via C-mouse hovering.
+this is guarded by the configuration options "show_consts_markup"
+(default true) and "show_markup" (default true for PIDE interaction).
+Ast translation rules (command 'translations') and mixfix notation work
+with or without such extra constraints, but ML translation functions
+(command 'print_ast_translation') need may need to be changed slightly.
+Rare INCOMPATIBILITY. The Prover IDE displays type constraints for
+constants as for variables, e.g. via C-mouse hovering.
* The Simplifier now supports special "congprocs", using keyword
'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML