doc-src/TutorialI/Recdef/Induction.thy
changeset 10196 4d1af711cf7b
parent 10171 59d6633835fa
child 10362 c6b197ccf1f1