src/HOL/Conditionally_Complete_Lattices.thy
changeset 56958 b2c2f74d1c93
parent 56218 1c3f1f2431f9
child 57275 0ddb5b755cdc