src/Doc/Tutorial/Recdef/Nested2.thy
changeset 82986 951e009e20f4
parent 69505 cc2d676d5395