[isabelle-dev] NEWS: ML antiquotation @{print}

[Makarius]

* ML antiquotation @{print} inlines a function to print an arbitrary
ML value, which is occasionally useful for diagnostic or demonstration
purposes.


This refers to Isabelle/386e4cb7ad68, which also points to the place where 
the older antiquotation @{make_string} is documented.

Despite these official Isabelle/ML tools for debugging and diagnostics, I 
sometimes see low-level ML traditionalists who are stuck with PolyML.print 
or PolyML.makestring -- but there are no reasons for that, apart from old 
habits.  David Matthews has provided better entry points for that several 
years ago, and the above antiquotations make use of them.


 	Makarius