doc-src/TutorialI/Recdef/examples.thy
changeset 10849 de981d0037ed
parent 10654 458068404143
child 11160 e0ab13bec5c8