src/HOL/Tools/function_package/fundef_core.ML
changeset 26477 ecf06644f6cb
parent 26196 0a0c2752561e
child 26529 03ad378ed5f0
equal deleted inserted replaced
26476:4e78281b3273 26477:ecf06644f6cb