src/Doc/Tutorial/Fun/fun0.thy
changeset 64242 93c6f0da5c70
parent 62392 747d36865c2c
child 67406 23307fd33906