src/HOL/Algebra/Lattice.thy
changeset 14750 8f1ee65bd3ea
parent 14706 71590b7733b7
child 14751 0d7850e27fed