src/HOL/Tools/function_package/fundef_common.ML
changeset 19759 2d0896653e7a
parent 19617 7cb4b67d4b97
child 19770 be5c23ebe1eb