src/HOL/Fun.thy
changeset 9030 bb7622789bf2
parent 8960 0cd01ec1830b
child 9141 49f6e45e7199