src/HOL/Algebra/Lattice.thy
changeset 72567 aeac6424d3b5
parent 69700 7a92cbec7030
child 77362 1a6103f6ab0b