src/HOL/Fun.thy
changeset 10168 50be659d4222
parent 9352 416b2ecd97a1
child 10212 33fe2d701ddd