* Indexing of literal facts: be more serious about including only facts from the visible specification/proof context, but not the background context (locale etc.). Affects `prop` notation and method "fact". INCOMPATIBILITY: need to name facts explicitly in rare situations.
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Florian Haftmann
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Brian Huffman
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Lawrence Paulson
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Lawrence Paulson
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius
- [isabelle-dev] NEWS Makarius