doc-src/TutorialI/Recdef/Induction.thy
changeset 45907 4b41967bd77e
parent 16417 9bc16273c2d4