src/HOL/IMP/Def_Init_Exp.thy
changeset 50267 1da2e67242d6
parent 50161 4fc4237488ab
child 53015 a1119cf551e8