src/HOL/Complete_Lattice.thy
changeset 32777 8ae3a48c69d9
parent 32678 de1f7d4da21a
child 32879 7f5ce7af45fd