doc-src/TutorialI/Recdef/Induction.thy
changeset 47432 e1576d13e933
parent 16417 9bc16273c2d4