src/HOL/Fun.thy
changeset 74925 4bc306cb2832
parent 74123 7c5842b06114
child 75582 6fb4a0829cc4