src/HOL/Fun.thy
changeset 28436 4faf705a177d
parent 27330 1af2598b5f7d
child 28562 4e74209f113e