src/HOL/Tools/Function/fundef.ML
changeset 33097 9d501e11084a
parent 33056 791a4655cae3