src/HOL/IMP/Def_Init.thy
changeset 75097 7001ae6c0832
parent 53015 a1119cf551e8