Skip to content
Success

Changes

Summary

  1. discontinued theory-local special syntax for lattice orderings
  2. keep locale lifting rules on the global level
Changeset 63820:9f004fbf9d5c by haftmann:
discontinued theory-local special syntax for lattice orderings
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
Changeset 63819:58f74e90b96d by haftmann:
keep locale lifting rules on the global level
The file was modified src/HOL/Orderings.thy (diff)