doc-src/TutorialI/Recdef/Nested2.thy
changeset 45272 5995ab88a00f
parent 40878 7695e4de4d86