[isabelle-dev] NEWS: 'alias' and 'type_alias'
makarius at sketis.net
Mon Jul 3 15:08:49 CEST 2017
*** 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.
More information about the isabelle-dev