doc-src/TutorialI/Recdef/Nested2.thy
changeset 45750 17100f4ce0b5
parent 40878 7695e4de4d86