doc-src/TutorialI/Recdef/Induction.thy
changeset 25231 1aa9c8f022d0
parent 16417 9bc16273c2d4