src/HOL/Tools/function_package/fundef_core.ML
changeset 24434 c588ec4cf194
parent 24168 86a03a092062
child 24510 6c612357cf3d