src/HOL/IMP/Def_Init_Exp.thy
changeset 50655 1656248e673f
parent 50161 4fc4237488ab
child 53015 a1119cf551e8