src/HOL/Library/Lub_Glb.thy
changeset 78941 bc7b7357f4bc
parent 69597 ff784d5a5bfb