src/HOL/Fun.thy
changeset 4208 b67223fddc11
parent 4059 59c1422c9da5
child 4648 f04da668581c