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

Lars Noschinski noschinl at in.tum.de
Fri Apr 4 13:17:26 CEST 2014

So what should I use before antiquotations are available? Should I still avoid PolyML.makestring?

Makarius <makarius at sketis.net> schrieb:

>* ML antiquotation @{print} inlines a function to print an arbitrary
>ML value, which is occasionally useful for diagnostic or demonstration
>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
>isabelle-dev mailing list
>isabelle-dev at in.tum.de

More information about the isabelle-dev mailing list