src/HOL/Fun.thy
changeset 49768 3ecfba7e731d
parent 49739 13aa6d8268ec
child 49905 a81f95693c68