src/HOL/IMP/Def_Init_Sound_Small.thy
changeset 51267 c68c1b89a0f1
parent 50161 4fc4237488ab
child 51466 d53cdbca1be4