[isabelle-dev] NEWS: Thm.pretty_thm etc.

[Makarius]

*** ML ***

* The auxiliary module Pure/display.ML has been eliminated. Its
elementary thm print operations are now in Pure/more_thm.ML and thus
called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.


This refers to abe08fb15a12.  Pure/display.ML used to be an add-on to 
thm.ML, but that is now more_thm.ML.  Note that it is difficult to work 
with a proper proof context deep down there: most print operations are now 
elsewhere.


 	Makarius