src/HOL/Fun.thy
changeset 10447 1dbd79bd3bc6
parent 10212 33fe2d701ddd
child 10826 f3b7201dda27