src/Doc/Tutorial/Recdef/Nested0.thy
changeset 78069 e5bd9b3c6f0f
parent 67406 23307fd33906