src/HOL/IMP/Denotational.thy
changeset 59702 58dfaa369c11
parent 58889 5b7a9633cfa8
child 62217 527488dc8b90