src/HOL/Fun.thy
changeset 3333 0bbf06e86c06
parent 2912 3fac3e8d5d3e
child 4059 59c1422c9da5