src/HOL/Tools/function_package/fundef_common.ML
changeset 24434 c588ec4cf194
parent 24171 25381ce95316
child 24920 2a45e400fdad
equal deleted inserted replaced
24433:4a405457e9d6 24434:c588ec4cf194