src/Doc/Tutorial/Fun/fun0.thy
changeset 66627 4145169ae609
parent 62392 747d36865c2c
child 67406 23307fd33906