src/HOL/IMP/Def_Init_Small.thy
changeset 50267 1da2e67242d6
parent 50161 4fc4237488ab
child 52046 bc01725d7918