src/Doc/Tutorial/Recdef/examples.thy
changeset 60370 9ec1d3d2068e
parent 58860 fee7cfa69c50
child 67406 23307fd33906