florian.haftmann at informatik.tu-muenchen.de
Tue Oct 16 23:15:10 CEST 2007
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
perl -i -pe 's/\\<\^loc>//g;' THYFILENAME1 THYFILENAME2 ...
- 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 249 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev