src/Doc/Tutorial/Fun/fun0.thy
changeset 60417 014d77e5c1ab
parent 58860 fee7cfa69c50
child 62392 747d36865c2c
equal deleted inserted replaced
60416:e1ff959f4f1b 60417:014d77e5c1ab