src/HOL/Fun.thy
changeset 73439 cb127ce2c092
parent 73328 ff24fe85ee57
child 73466 ee1c4962671c