src/HOL/IMP/Denotation.thy
changeset 49007 f781bbe0d91b
parent 45015 fdac1e9880eb
child 52046 bc01725d7918