src/HOL/Tools/function_package/fundef_lib.ML
changeset 23277 aa158e145ea3
parent 23260 eb6d86fb7ed3
child 23819 2040846d1bbe