src/HOL/Fun.thy
changeset 23830 f838adde842d
parent 23738 3a801ffdc58c
child 23878 bd651ecd4b8a