src/HOL/Conditionally_Complete_Lattices.thy
changeset 70708 3e11f35496b3
parent 69611 42cc3609fedf
child 71096 ec7cc76e88e5