src/HOL/Tools/function_package/fundef_package.ML
changeset 24930 cc2e0e8c81af
parent 24867 e5b55d7be9bb
child 24977 9f98751c9628