src/HOL/Fun.thy
changeset 55101 57c875e488bd
parent 55066 4e5ddf3162ac
child 55414 eab03e9cee8a