src/HOL/Conditionally_Complete_Lattices.thy
changeset 58476 6ade4c7109a8
parent 57447 87429bdecad5
child 58889 5b7a9633cfa8