src/HOL/IMP/Def_Init_Exp.thy
changeset 51722 3da99469cc1b
parent 50161 4fc4237488ab
child 53015 a1119cf551e8