src/HOL/Fun.ML
changeset 2981 aa5aeb6467c6
parent 2935 998cb95fdd43
child 3341 89fe22bf9f54