doc-src/TutorialI/Recdef/examples.thy
changeset 10589 b2d1b393b750
parent 10362 c6b197ccf1f1
child 10654 458068404143