src/HOL/Analysis/Linear_Algebra.thy
 changeset 67399 eab6ce8368fa parent 66804 3f9bb52082c4 child 67443 3abf6a722518
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 10 15:21:49 2018 +0100
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 10 15:25:09 2018 +0100
1.3 @@ -980,7 +980,7 @@
1.4        by (intro sum.mono_neutral_cong_left) (auto intro: X)
1.5      also have "\<dots> = (\<Sum>z\<in>{z. X x z \<noteq> 0}. X x z *\<^sub>R z) + (\<Sum>z\<in>{z. X y z \<noteq> 0}. X y z *\<^sub>R z)"
1.7 -               intro!: arg_cong2[where f="op +"]  sum.mono_neutral_cong_right X)
1.8 +               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
1.9      also have "\<dots> = x + y"
1.11      also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
1.12 @@ -1024,7 +1024,7 @@
1.13      show "g (x + y) = g x + g y"
1.16 -               intro!: arg_cong2[where f="op +"]  sum.mono_neutral_cong_right X)
1.17 +               intro!: arg_cong2[where f="(+)"]  sum.mono_neutral_cong_right X)
1.18    next
1.19      show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x
1.20        by (auto simp add: g_def X_cmult scaleR_sum_right intro!: sum.mono_neutral_cong_left X)
1.21 @@ -1398,7 +1398,7 @@