src/HOL/IMP/Def_Init_Exp.thy
changeset 52839 2c0e1a84dcc7
parent 50161 4fc4237488ab
child 53015 a1119cf551e8