src/HOL/Conditionally_Complete_Lattices.thy
changeset 71185 8a0e25d93a95
parent 71096 ec7cc76e88e5
child 71238 9612115e06d1