src/HOL/Tools/function_package/auto_term.ML
changeset 27018 b3e63f39fc0f
parent 25545 21cd20c1ce98
child 30510 4120fc59dd85
equal deleted inserted replaced
27017:1e0e8c1adf8c 27018:b3e63f39fc0f