doc-src/TutorialI/Recdef/examples.thy
changeset 10274 130ff5eb2b80
parent 9933 9feb1e0c4cb3
child 10362 c6b197ccf1f1
equal deleted inserted replaced
10273:59570adf2d3c 10274:130ff5eb2b80