src/HOL/Fun.thy
changeset 33242 99577c7085c8
parent 33057 764547b68538
child 33318 ddd97d9dfbfb