src/HOL/Recdef.thy
changeset 15291 dd4648ae6eff
parent 15150 c7af682b9ee5
child 15481 fc075ae929e4