src/HOL/Conditionally_Complete_Lattices.thy
changeset 77509 3bc49507bae5
parent 76770 04d7c8496b3d
child 77934 01c88cf514fc