src/HOL/Algebra/Lattice.thy
changeset 72546 58b1826354c9
parent 69700 7a92cbec7030
child 77362 1a6103f6ab0b