src/HOL/Fun.thy
changeset 28131 3130d7b3149d
parent 27330 1af2598b5f7d
child 28562 4e74209f113e