src/HOL/IMP/Def_Init_Small.thy
changeset 81449 d92d754b5dd9
parent 80914 d97fdabd9e2b