src/HOL/IMP/Def_Init_Small.thy
changeset 66787 64b47495676d
parent 63540 f8652d0534fa
child 67406 23307fd33906