doc-src/TutorialI/Recdef/Induction.thy
changeset 10396 5ab08609e6c8
parent 10362 c6b197ccf1f1
child 10795 9e888d60d3e5