src/HOL/Fun.thy
changeset 62764 ff3b8e4079bd
parent 62618 f7f2467ab854
child 62843 313d3b697c9a