src/HOL/Tools/function_package/fundef_lib.ML
changeset 20535 b4b3933ec026
parent 20523 36a59e5d0039
child 20851 bf80cb83f8be