src/HOL/Fun.thy
changeset 22175 d9e3e4c30d6b
parent 21906 db805c70a519
child 22453 530db8c36f53