[isabelle-dev] NEWS

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Jul 2 07:53:11 CEST 2008

New ML antiquotation 'code': takes constant as argument, generates
corresponding code in background and inserts name of the corresponding
resulting ML value/function/datatype constructor binding in place.  All
occurences of 'code' with a single ML block are generated simultaneously.
Provides a generic and safe interface for instrumentalizing code
generation.  See HOL/ex/Code_Antiq for a toy example, or
HOL/Complex/ex/ReflectedFerrack  for a more ambitious application.  In
future you ought refrain from  ad-hoc compiling generated SML code on
the ML toplevel.
Note that (for technical reasons) 'code' cannot refer to constants for
which user-defined serializations are set.  Refer to the corresponding
ML counterpart directly in that cases.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080702/07ee4551/attachment.sig>

More information about the isabelle-dev mailing list