src/HOL/Tools/function_package/fundef_package.ML
changeset 23512 770e7f9f715b
parent 23473 997bca36d4fe
child 23819 2040846d1bbe