doc-src/TutorialI/Recdef/examples.thy
changeset 13922 75ae4244a596
parent 11705 ac8ca15c556c
child 15905 0a4cc9b113c7
equal deleted inserted replaced
13921:69c627b6b28d 13922:75ae4244a596