src/Doc/Tutorial/Fun/fun0.thy
changeset 62101 26c0a70f78a3
parent 58860 fee7cfa69c50
child 62392 747d36865c2c