doc-src/TutorialI/Recdef/Induction.thy
changeset 11145 3e47692e3a3e
parent 10971 6852682eaf16
child 11159 07b13770c4d6