doc-src/TutorialI/Recdef/Induction.thy
changeset 44369 02e13192a053
parent 16417 9bc16273c2d4