src/HOL/Algebra/Lattice.thy
changeset 77784 4046731cfa6c
parent 77362 1a6103f6ab0b
child 80768 c7723cc15de8