--- 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