src/HOL/Fun.thy
changeset 15618 05bad476e0f0
parent 15531 08c8dad8e399
child 15691 900cf45ff0a6