Summary
- clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;
- tuned;
- less redundant exploration of full name space;
- tuned;
- avoid multiple reports on shared type;
The file was modified | src/Tools/jEdit/src/rendering.scala (diff) |
The file was modified | src/HOL/Induct/Common_Patterns.thy (diff) |
The file was modified | src/HOL/Induct/Sigma_Algebra.thy (diff) |
The file was modified | src/Pure/General/name_space.ML (diff) |
The file was modified | src/Pure/General/name_space.ML (diff) |
The file was modified | src/Pure/Isar/parse.ML (diff) |