doc-src/TutorialI/Recdef/examples.thy
changeset 9145 9f7b8de5bfaf
parent 8771 026f37a86ea7
child 9541 d17c0b34d5c8
equal deleted inserted replaced
9144:20a70ef9c320 9145:9f7b8de5bfaf