Summary
- discontinued theory-local special syntax for lattice orderings
- keep locale lifting rules on the global level
The file was modified | src/HOL/Complete_Lattices.thy (diff) |
The file was modified | src/HOL/Lattices.thy (diff) |
The file was modified | src/HOL/Orderings.thy (diff) |