doc-src/TutorialI/Recdef/examples.thy
changeset 10795 9e888d60d3e5
parent 10654 458068404143
child 11160 e0ab13bec5c8