src/HOL/IMP/Def_Init_Small.thy
changeset 82488 b52e57ed7e29
parent 80914 d97fdabd9e2b