Nominal/nominal_function.ML
changeset 2997 132575f5bd26
parent 2992 782a2cd1a8d0
child 2999 68c894c513f6