src/HOL/IMP/Denotational.thy
changeset 75565 65a2482f772d
parent 69661 a03a63b81f44