doc-src/TutorialI/Recdef/examples.thy
changeset 14706 71590b7733b7
parent 11705 ac8ca15c556c
child 15905 0a4cc9b113c7
equal deleted inserted replaced
14705:14b2c22a7e40 14706:71590b7733b7