src/Doc/Tutorial/Recdef/examples.thy
changeset 60523 be2d9f5ddc76
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
60522:1409b4015671 60523:be2d9f5ddc76