doc-src/TutorialI/Recdef/Nested1.thy
changeset 9812 87ba969d069c
parent 9792 bbefb6ce5cb2
child 9834 109b11c4e77e