src/HOL/Fun.thy
changeset 11371 1d5d181b7e28
parent 11123 15ffc08f905e
child 11451 8abfb4f7bd02