src/HOL/Tools/Function/function_core.ML
changeset 55639 e4e8cbd9d780
parent 55396 91bc9f69a958
child 55990 41c6b99c5fb7