src/HOL/IMP/Denotational.thy
changeset 58993 302104d8366b
parent 58889 5b7a9633cfa8
child 62217 527488dc8b90