src/HOL/Tools/function_package/fundef_lib.ML
changeset 26477 ecf06644f6cb
parent 24584 01e83ffa6c54
child 27330 1af2598b5f7d
equal deleted inserted replaced
26476:4e78281b3273 26477:ecf06644f6cb