src/HOL/Tools/function_package/fundef_lib.ML
changeset 23277 aa158e145ea3
parent 23260 eb6d86fb7ed3
child 23819 2040846d1bbe
equal deleted inserted replaced
23276:a70934b63910 23277:aa158e145ea3