src/HOL/IMP/Def_Init.thy
changeset 55770 f2cf7f92c9ac
parent 53015 a1119cf551e8