src/HOL/IMP/Complete_Lattice.thy
changeset 49007 f781bbe0d91b
parent 48759 ff570720ba1c
child 49487 7e7ac4956117