src/HOL/Tools/function_package/fundef_core.ML
changeset 24930 cc2e0e8c81af
parent 24693 fe88913f3706
child 24960 39d1dd215d73