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