[isabelle-dev] NEWS

[Florian Haftmann]

Class-context aware syntax for class target ("user space type system"):

Local operations in class context (fixes, definitions, axiomatizations,
abbreviations) are identified with their global counterparts during
reading and printing of terms.  Practically, this allows to use the same
syntax for both local *and* global operations.  Syntax declarations
referring directly to local fixes, definitions, axiomatizations and
abbreviations are applied to their global counterparts instead (but
explicit notation declarations still are local); the special treatment
of \<^loc> in local syntax declarations has been abandoned.

INCOMPATIBILITY.  Most affected theories shall work after the following
purgatory:

    perl -i -pe 's/\\<\^loc>//g;' THYFILENAME1 THYFILENAME2 ...

Current limitations:
- printing of local abbreviations sometimes yields unexpected results.
- some facilities (e.g. attribute of, legacy tac-methods) still do not
use canonical interfaces for printing and reading terms.


	Florian

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