doc-src/TutorialI/Recdef/Induction.thy
changeset 46598 fd0ac848140e
parent 16417 9bc16273c2d4