src/HOL/Fun.thy
changeset 3257 4e3724e0659f
parent 2912 3fac3e8d5d3e
child 4059 59c1422c9da5