doc-src/TutorialI/Recdef/Induction.thy
changeset 43117 5de84843685f
parent 16417 9bc16273c2d4
equal deleted inserted replaced
43116:e0add071fa10 43117:5de84843685f