licenses: convert license tags to SPDX

lib: avoid use of Local_Theory.reset

Local_Theory.reset is about to be discontinued in the next Isabelle release

lib: an abbreviation command with pretty printing inside locales

Normal abbreviations are not contracted on pretty printing when defined
inside a locale. This commit provide the command locale_abbrev which does
contract on pretty print even when defined inside a locale. It cannot be
used with abbreviations that mention fixed locale variables (whereas the
standard abbreviations can).

Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>