doc-src/TutorialI/Recdef/Nested1.thy
changeset 27147 62ab1968c1f4
parent 16417 9bc16273c2d4