doc-src/TutorialI/Recdef/Induction.thy
changeset 10668 3b84288e60b7
parent 10362 c6b197ccf1f1
child 10795 9e888d60d3e5