[isabelle-dev] NEWS

[Florian Haftmann]

Different bookkeeping for code equations: 

a) On theory merge, the last set of code equations for a particular
   constant is taken (in accordance with the policy applied by other
   parts of the code generator framework).
b) Code equations stemming from explicit declarations (e.g. code
   attribute) gain priority over default code equations stemming from
   definition, primrec, fun etc.
INCOMPATIBILITY.

	Florian

--=20

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_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/20080905/282a29c2/attachment.sig>