NEWS: Clarified semantics for adding code equations

[Florian Haftmann]

In 2865a6618cba the semantics for adding code equations has been 
clarified and also (for the first time) documented as such:

* Code equations from preceding theories are superseded.
* Code equations declared in the course of a theory are appended, not 
prepended.

This allows to write down code equations in a »natural« order as you 
would expect in a functional programming language.

For the case that an application needs transition, you may use
		
   declare [[code_prepend_allowed]] – ‹vanishes at end of theory›

   lemma [code prepend]:
     …

to use the former prepend semantics. This is only a device for migration 
and will vanish sooner or later.

It is anyway very unlikely that this is actually needed – during the 
migration of existing theories it turned out that most code equations 
are declared in »natural« order anyway, which now fits perfectly to the 
clarified semantics.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250627/9f21638d/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250627/9f21638d/attachment-0001.sig>