src/Doc/Tutorial/Fun/fun0.thy
changeset 58719 ac4f764c5be1
parent 58620 7435b6a3f72e
child 58860 fee7cfa69c50