src/HOL/Conditionally_Complete_Lattices.thy
changeset 77809 8ee97b3841cc
parent 76770 04d7c8496b3d
child 77934 01c88cf514fc