src/HOL/Tools/Function/function_core.ML
changeset 39071 928c5a5bdc93
parent 38920 39db63c45683
child 39288 f1ae2493d93f