src/HOL/Library/Finite_Lattice.thy
changeset 78366 aa4ea5398ab8
parent 77811 ae9e6218443d