src/HOL/IMP/Denotation.thy
changeset 51593 d40aec502416
parent 45015 fdac1e9880eb
child 52046 bc01725d7918