src/HOL/Fun.ML
changeset 8765 1bc30ff5fc54
parent 8309 a054d5c98b21
child 8767 eae30939b592