src/HOL/IMP/Denotational.thy
changeset 62214 451bd09b8277
parent 58889 5b7a9633cfa8
child 62217 527488dc8b90