src/Doc/Tutorial/Recdef/examples.thy
changeset 66823 f529719cc47d
parent 58860 fee7cfa69c50
child 67406 23307fd33906