src/HOL/Fun.thy
changeset 6260 a8010d459ef7
parent 6171 cd237a10cbf8
child 7374 dec7b838f5cb