src/HOL/Fun.thy
changeset 55400 1e8dd9cd320b
parent 55066 4e5ddf3162ac
child 55414 eab03e9cee8a