src/HOL/Algebra/Lattice.thy
changeset 14747 2eaff69d3d10
parent 14706 71590b7733b7
child 14751 0d7850e27fed