[isabelle-dev] NEWS

[Florian Haftmann]

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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>