NEWS
changeset 49699 1301ed115729
parent 49647 21ae8500d261
child 49738 1e1611fd32df
--- a/NEWS	Thu Oct 04 11:45:56 2012 +0200
+++ b/NEWS	Thu Oct 04 13:56:32 2012 +0200
@@ -16,6 +16,11 @@
     . more plugin options and preferences, based on Isabelle/Scala;
     . uniform Java 7 platform on Linux, Mac OS X, Windows;
 
+* Configuration option show_markup controls direct inlining of markup
+into the printed representation of formal entities --- notably type
+and sort constraints.  This enables Prover IDE users to retrieve that
+information via tooltips in the output window, for example.
+
 * Command 'ML_file' evaluates ML text from a file directly within the
 theory, without any predeclaration via 'uses' in the theory header.