src/HOL/Conditionally_Complete_Lattices.thy
changeset 76684 3eda063a20a4
parent 75669 43f5dfb7fa35
child 76770 04d7c8496b3d