doc-src/TutorialI/Recdef/examples.thy
changeset 13078 1dd711c6b93c
parent 11705 ac8ca15c556c
child 15905 0a4cc9b113c7
equal deleted inserted replaced
13077:c2e4d9990162 13078:1dd711c6b93c