doc-src/TutorialI/Recdef/Induction.thy
changeset 38937 1b1a2f5ccd7d
parent 16417 9bc16273c2d4