src/HOL/Fun.thy
changeset 32842 98702c579ad0
parent 32740 9dd0a2f83429
child 32961 61431a41ddd5