diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -142,13 +142,13 @@
 
 instantiation vec :: (plus, finite) plus
 begin
-  definition "op + \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))"
+  definition "(+) \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))"
   instance ..
 end
 
 instantiation vec :: (minus, finite) minus
 begin
-  definition "op - \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))"
+  definition "(-) \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))"
   instance ..
 end