[isabelle-dev] NEWS: Thm.pretty_thm etc.
makarius at sketis.net
Sat Sep 26 00:17:01 CEST 2015
*** 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
More information about the isabelle-dev