src/HOL/Conditionally_Complete_Lattices.thy
changeset 60544 3daf5eacec05
parent 60172 423273355b55
child 60615 e5fa1d5d3952