doc-src/TutorialI/Recdef/examples.thy
changeset 15759 144c9f9a8ade
parent 11705 ac8ca15c556c
child 15905 0a4cc9b113c7
equal deleted inserted replaced
15758:07e382399a96 15759:144c9f9a8ade