src/HOL/Conditionally_Complete_Lattices.thy
changeset 77050 92509e4274eb
parent 76770 04d7c8496b3d
child 77934 01c88cf514fc