src/Doc/Tutorial/Recdef/examples.thy
changeset 65267 7e427dff15dd
parent 58860 fee7cfa69c50
child 67406 23307fd33906