src/HOL/Conditionally_Complete_Lattices.thy
changeset 57204 7c36ce8e45f6
parent 56218 1c3f1f2431f9
child 57275 0ddb5b755cdc