src/HOL/Fun.thy
changeset 44262 355d5438f5fb
parent 43991 f4a7697011c5
child 44277 bcb696533579