src/Doc/Tutorial/Fun/fun0.thy
changeset 58872 f0f623005324
parent 58860 fee7cfa69c50
child 62392 747d36865c2c
equal deleted inserted replaced
58871:c399ae4b836f 58872:f0f623005324