src/HOL/IMP/Denotation.thy
changeset 43158 686fa0a0696e
parent 43144 631dd866b284
child 45015 fdac1e9880eb