doc-src/TutorialI/Recdef/Nested2.thy
changeset 46598 fd0ac848140e
parent 40878 7695e4de4d86