src/Doc/Tutorial/Recdef/examples.thy
changeset 59075 9f87eb298b75
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
59074:7836d927ffca 59075:9f87eb298b75