doc-src/TutorialI/Recdef/Nested2.thy
changeset 41049 0edd245892ed
parent 40878 7695e4de4d86