Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;
  2. tuned;
  3. less redundant exploration of full name space;
  4. tuned;
  5. avoid multiple reports on shared type;
Changeset 63234:2eb2ff479cfe by wenzelm:
clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;
The file was modified src/Tools/jEdit/src/rendering.scala (diff)
Changeset 63233:e53830948c4f by wenzelm:
tuned;
The file was modified src/HOL/Induct/Common_Patterns.thy (diff)
The file was modified src/HOL/Induct/Sigma_Algebra.thy (diff)
Changeset 63232:7238ed9a27ab by wenzelm:
less redundant exploration of full name space;
The file was modified src/Pure/General/name_space.ML (diff)
Changeset 63231:54197a7c1bbd by wenzelm:
tuned;
The file was modified src/Pure/General/name_space.ML (diff)
Changeset 63230:ae5275fa96dc by wenzelm:
avoid multiple reports on shared type;
The file was modified src/Pure/Isar/parse.ML (diff)