src/HOL/Library/Finite_Lattice.thy
changeset 80861 9de19e3a7231
parent 77811 ae9e6218443d