src/HOL/IMP/Def_Init_Sound_Small.thy
changeset 52587 067f1f950dc8
parent 52120 e6433b34364b