src/HOL/Tools/function_package/fundef_common.ML
changeset 27376 ffe9b958bada
parent 26989 9b2acb536228
child 28083 103d9282a946