Nominal/nominal_function.ML
changeset 2995 6d2859aeebba
parent 2992 782a2cd1a8d0
child 2999 68c894c513f6
equal deleted inserted replaced
2994:4ee772b12032 2995:6d2859aeebba