src/HOL/Tools/Function/function_core.ML
changeset 39034 ebeb48fd653b
parent 38920 39db63c45683
child 39288 f1ae2493d93f