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

Makarius 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 mailing list