doc-src/TutorialI/Recdef/examples.thy
changeset 10795 9e888d60d3e5
parent 10654 458068404143
child 11160 e0ab13bec5c8
equal deleted inserted replaced
10794:65d18005d802 10795:9e888d60d3e5