doc-src/TutorialI/Recdef/examples.thy
changeset 11420 9529d31f39e0
parent 11231 30d96882f915
child 11458 09a6c44a48ea
equal deleted inserted replaced
11419:9577530e8a5a 11420:9529d31f39e0