doc-src/TutorialI/Recdef/examples.thy
changeset 13845 5a04de077a9f
parent 11705 ac8ca15c556c
child 15905 0a4cc9b113c7
equal deleted inserted replaced
13844:44f741cdcea3 13845:5a04de077a9f