* Name bindings in higher specification mechanisms (notably LocalTheory.define, LocalTheory.note, and derived packages) are now formalized as type Name.binding, replacing old bstring. INCOMPATIBILITY, need to wrap strings via Name.binding function, see also Name.name_of. Packages should pass name bindings given by the user to underlying specification mechanisms; this enables precise tracking of source positions, for example.
- [isabelle-dev] HOL vs. HOL-Com... Makarius
- [isabelle-dev] HOL vs. HOL-Com... Lawrence Paulson
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Amine Chaieb
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Tobias Nipkow
- [isabelle-dev] NEWS Michael Nedzelsky
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Tobias Nipkow
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius