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