src/HOL/Tools/function_package/fundef_package.ML
changeset 29477 b834f95c2532
parent 29051 b9c5726e79ab
child 29581 b3b33e0298eb