src/HOL/Tools/function_package/fundef_common.ML
changeset 26088 9b48d0264ffd
parent 25558 5c317e8f5673
child 26529 03ad378ed5f0