| changeset 67399 | eab6ce8368fa |
| parent 66154 | bc5e6461f759 |
| child 67685 | bdff8bf0a75b |
--- a/src/HOL/Analysis/Euclidean_Space.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Analysis/Euclidean_Space.thy Wed Jan 10 15:25:09 2018 +0100 @@ -242,7 +242,7 @@ lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)" unfolding Basis_prod_def - by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI) + by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="(+)"] inj_onI) end