src/HOL/Fun.thy
changeset 15564 c899efea601f
parent 15531 08c8dad8e399
child 15691 900cf45ff0a6