src/HOL/Tools/Function/fun.ML
changeset 54938 8cccfb8f1d36
parent 54407 e95831757903
child 56254 a2dd9200854d