src/HOL/IMP/Denotational.thy
changeset 79271 b14b289caaf6
parent 69661 a03a63b81f44