*** 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
