[isabelle-dev] NEWS: 'alias' and 'type_alias'

[Makarius]

*** General ***

* Commands 'alias' and 'type_alias' introduce aliases for constants and
type constructors, respectively. This allows adhoc changes to name-space
accesses within global or local theory contexts, e.g. within a 'bundle'.


This refers to Isabelle/df85956228c2. These are fully localized
commands, in contrast to the very old-fashioned hide_const, hide_type etc.

Maybe this occasionally helps to sort out name space confusion, although
it is probably a feature of last resort.


	Makarius