src/HOL/Conditionally_Complete_Lattices.thy
changeset 60517 f16e4fb20652
parent 60172 423273355b55
child 60615 e5fa1d5d3952