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

Makarius makarius at sketis.net
Fri Apr 4 13:33:39 CEST 2014

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.


More information about the isabelle-dev mailing list