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

Makarius 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 mailing list