src/HOL/Fun.thy
changeset 9738 2e1dca5af2d4
parent 9352 416b2ecd97a1
child 10212 33fe2d701ddd