*** 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
