src/Doc/Tutorial/Recdef/Nested1.thy
changeset 60614 e39e6881985c
parent 56846 9df717fef2bb
child 67406 23307fd33906