src/HOL/Library/Lub_Glb.thy
changeset 82336 1d0116b288e3
parent 69597 ff784d5a5bfb