src/HOL/Fun.thy
changeset 73424 2b657a70116c
parent 73328 ff24fe85ee57
child 73466 ee1c4962671c