src/HOL/Tools/function_package/fundef_core.ML
changeset 27249 f339dc43ce9f
parent 27115 0dcafa5c9e3f
child 27336 88f1e557f712