src/HOL/Conditionally_Complete_Lattices.thy
changeset 52657 42c14dba1daa
parent 52265 bb907eba5902
child 53215 5e47c31c6f7c