src/HOL/Tools/function_package/fundef_core.ML
changeset 28998 23cbaa9f9834
parent 28965 1de908189869
child 29265 5b4247055bd7