src/HOL/Fun.thy
changeset 27885 76b51cd0a37c
parent 27330 1af2598b5f7d
child 28562 4e74209f113e