doc-src/TutorialI/Recdef/Induction.thy
changeset 19831 c00e04f8a52a
parent 16417 9bc16273c2d4