src/HOL/Tools/function_package/fundef_lib.ML
changeset 28998 23cbaa9f9834
parent 28965 1de908189869
child 29125 d41182a8135c