doc-src/TutorialI/Recdef/examples.thy
changeset 15898 435f0e743854
parent 11705 ac8ca15c556c
child 15905 0a4cc9b113c7
equal deleted inserted replaced
15897:86d510b0e4b7 15898:435f0e743854