src/HOL/IMP/Complete_Lattice.thy
changeset 74376 1cc630940147
parent 68778 4566bac4517d