src/Doc/Tutorial/Recdef/Nested1.thy
changeset 81285 34f3ec8d4d24
parent 69505 cc2d676d5395