doc-src/TutorialI/Recdef/Nested2.thy
changeset 45967 76cf71ed15c7
parent 40878 7695e4de4d86