src/Doc/Tutorial/Fun/fun0.thy
changeset 60480 459f5e017e77
parent 58860 fee7cfa69c50
child 62392 747d36865c2c
equal deleted inserted replaced
60479:db238135f386 60480:459f5e017e77