src/HOL/Tools/function_package/fundef_common.ML
changeset 22012 adf68479ae1b
parent 21835 84fd5de0691c
child 22166 0a50d4db234a