src/HOL/Library/Lub_Glb.thy
changeset 80321 31b9dfbe534c
parent 69597 ff784d5a5bfb