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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
