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

[Makarius]

On Fri, 4 Apr 2014, Lars Noschinski wrote:

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

All the documentation etc. is about Isabelle/ML user space, after Pure.thy 
is available.

For Isabelle/Pure bootstrap different rules apply -- quite complicated 
ones, because the bootstrap process changes the ML environment several 
times.  PolyML.makestring is here the main tool, down in the machine room, 
while you wear a blue overall and a helmet.


 	Makarius