src/HOL/Fun.thy
changeset 64715 33d5fa0ce6e5
parent 63591 8d20875f1290
child 64965 d55d743c45a2