src/HOL/Fun.thy
changeset 3816 7e1b695bcc5e
parent 2912 3fac3e8d5d3e
child 4059 59c1422c9da5