src/HOL/Tools/function_package/auto_term.ML
changeset 26973 6d52187fc2a6
parent 25545 21cd20c1ce98
child 30510 4120fc59dd85
equal deleted inserted replaced
26972:bde4289d793d 26973:6d52187fc2a6