Summary
- Improved error reporting when activating a locale instance (beyond syntax decls).
- Additional corollary Knaster_Tarski_idem_inf_eq.
The file was modified | src/Pure/Isar/locale.ML (diff) |
The file was modified | src/HOL/Algebra/Complete_Lattice.thy (diff) |