src/HOL/Conditionally_Complete_Lattices.thy
changeset 52593 aedf7b01c6e4
parent 52265 bb907eba5902
child 53215 5e47c31c6f7c