src/HOL/Conditionally_Complete_Lattices.thy
changeset 56493 1f660d858a75
parent 56218 1c3f1f2431f9
child 57275 0ddb5b755cdc