src/HOL/Conditionally_Complete_Lattices.thy
changeset 72425 d0937d55eb90
parent 71834 919a55257e62
child 73271 05a873f90655