src/HOL/Fun.thy
changeset 27389 823c7ec3ea4f
parent 27330 1af2598b5f7d
child 28562 4e74209f113e