src/HOL/Recdef.thy
changeset 10910 058775a575db
parent 10773 0deff0197496
child 11165 3b69feb7d053