src/HOL/IMP/Denotation.thy
changeset 44361 75ec83d45303
parent 43144 631dd866b284
child 45015 fdac1e9880eb