Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Improved error reporting when activating a locale instance (beyond syntax decls).
  2. Additional corollary Knaster_Tarski_idem_inf_eq.
Changeset 66188:bd841164592f by ballarin:
Improved error reporting when activating a locale instance (beyond syntax decls).
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 66187:85925d4ae93d by ballarin:
Additional corollary Knaster_Tarski_idem_inf_eq.
The file was modified src/HOL/Algebra/Complete_Lattice.thy (diff)