src/Doc/Tutorial/Recdef/Nested0.thy
changeset 83065 0a1a054d9b23
parent 67406 23307fd33906