src/HOL/Tools/function_package/fundef_package.ML
changeset 24403 b7c3ee2ca184
parent 24168 86a03a092062
child 24508 c8b82fec6447