src/HOL/Fun.thy
changeset 9066 b1e874e38dab
parent 8960 0cd01ec1830b
child 9141 49f6e45e7199