src/HOL/Conditionally_Complete_Lattices.thy
changeset 68983 caedabd2771c
parent 68610 4fdc9f681479
child 69275 9bbd5497befd