So what should I use before antiquotations are available? Should I still avoid PolyML.makestring?
Makarius <[email protected]> schrieb: >* 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 >_______________________________________________ >isabelle-dev mailing list >[email protected] >https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
