Prefix form of infix with * on either side no longer needs special treatment
authornipkow
Mon Sep 24 14:30:09 2018 +0200 (8 months ago)
changeset 690645840724b1d71
parent 69045 8c240fdeffcb
child 69065 440f7a575760
Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Sym_Groups.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Analysis/Ball_Volume.thy
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cartesian_Space.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Finite_Product_Measure.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Harmonic_Numbers.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Product_Vector.thy
src/HOL/Analysis/Riemann_Mapping.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/normarith.ML
src/HOL/Binomial.thy
src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Computational_Algebra/Polynomial.thy
src/HOL/Decision_Procs/Algebra_Aux.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Deriv.thy
src/HOL/Enum.thy
src/HOL/Factorial.thy
src/HOL/GCD.thy
src/HOL/Groups_List.thy
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Discrete.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Float.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Limits.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Modules.thy
src/HOL/Nonstandard_Analysis/HDeriv.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Totient.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/PMF_Impl.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
src/HOL/Real.thy
src/HOL/Real_Asymp/Multiseries_Expansion.thy
src/HOL/Real_Asymp/Real_Asymp_Approx.thy
src/HOL/Real_Asymp/exp_log_expression.ML
src/HOL/Real_Asymp/multiseries_expansion.ML
src/HOL/Real_Vector_Spaces.thy
src/HOL/SMT.thy
src/HOL/Set_Interval.thy
src/HOL/TLA/Intensional.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
src/HOL/Vector_Spaces.thy
src/HOL/Word/Word.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/ex/Transfer_Int_Nat.thy
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Sun Sep 23 21:49:31 2018 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Mon Sep 24 14:30:09 2018 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
     1.5  
     1.6  abbreviation int_ring :: "int ring" ("\<Z>")
     1.7 -  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
     1.8 +  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
     1.9  
    1.10  lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
    1.11    by simp
     2.1 --- a/src/HOL/Algebra/Sym_Groups.thy	Sun Sep 23 21:49:31 2018 +0200
     2.2 +++ b/src/HOL/Algebra/Sym_Groups.thy	Mon Sep 24 14:30:09 2018 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4    where "sym_group n = \<lparr> carrier = { p. p permutes {1..n} }, mult = (\<circ>), one = id \<rparr>"
     2.5  
     2.6  definition sign_img :: "int monoid"
     2.7 -  where "sign_img = \<lparr> carrier = { -1, 1 }, mult = ( * ), one = 1 \<rparr>"
     2.8 +  where "sign_img = \<lparr> carrier = { -1, 1 }, mult = (*), one = 1 \<rparr>"
     2.9  
    2.10  
    2.11  lemma sym_group_is_group: "group (sym_group n)"
     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Sep 23 21:49:31 2018 +0200
     3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Sep 24 14:30:09 2018 +0200
     3.3 @@ -1806,7 +1806,7 @@
     3.4  
     3.5  definition
     3.6    INTEG :: "int ring"
     3.7 -  where "INTEG = \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
     3.8 +  where "INTEG = \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
     3.9  
    3.10  lemma INTEG_cring: "cring INTEG"
    3.11    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
     4.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Sun Sep 23 21:49:31 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Mon Sep 24 14:30:09 2018 +0200
     4.3 @@ -147,7 +147,7 @@
     4.4         (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
     4.5    also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
     4.6                 (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
     4.7 -               \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close>
     4.8 +               \<partial>(distr lborel borel ((*) (1/r))))" using \<open>r > 0\<close>
     4.9      by (subst nn_integral_distr)
    4.10         (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
    4.11    also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * 
     5.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Sun Sep 23 21:49:31 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Mon Sep 24 14:30:09 2018 +0200
     5.3 @@ -1856,7 +1856,7 @@
     5.4  
     5.5    have sf[measurable]: "\<And>i. simple_function M (s' i)"
     5.6      unfolding s'_def using s(1)
     5.7 -    by (intro simple_function_compose2[where h="( *\<^sub>R)"] simple_function_indicator) auto
     5.8 +    by (intro simple_function_compose2[where h="(*\<^sub>R)"] simple_function_indicator) auto
     5.9  
    5.10    { fix i
    5.11      have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
     6.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sun Sep 23 21:49:31 2018 +0200
     6.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Sep 24 14:30:09 2018 +0200
     6.3 @@ -697,7 +697,7 @@
     6.4    by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
     6.5  
     6.6  
     6.7 -lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "( *\<^sub>R)"
     6.8 +lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "(*\<^sub>R)"
     6.9    by (rule bounded_linear_scaleR_right)
    6.10  declare blinfun_scaleR_right.rep_eq[simp]
    6.11  
    6.12 @@ -713,7 +713,7 @@
    6.13    by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
    6.14  
    6.15  
    6.16 -lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "( * )"
    6.17 +lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "(*)"
    6.18    by (rule bounded_linear_mult_right)
    6.19  declare blinfun_mult_right.rep_eq[simp]
    6.20  
     7.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Sep 23 21:49:31 2018 +0200
     7.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Sep 24 14:30:09 2018 +0200
     7.3 @@ -203,7 +203,7 @@
     7.4  lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
     7.5    shows "matrix(adjoint f) = transpose(matrix f)"
     7.6  proof%unimportant -
     7.7 -  have "matrix(adjoint f) = matrix(adjoint (( *v) (matrix f)))"
     7.8 +  have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
     7.9      by (simp add: lf)
    7.10    also have "\<dots> = transpose(matrix f)"
    7.11      unfolding adjoint_matrix matrix_of_matrix_vector_mul
    7.12 @@ -212,14 +212,14 @@
    7.13    finally show ?thesis .
    7.14  qed
    7.15  
    7.16 -lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
    7.17 +lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
    7.18    using matrix_vector_mul_linear[of A]
    7.19    by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
    7.20  
    7.21  lemma%unimportant (* FIX ME needs name*)
    7.22    fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
    7.23 -  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
    7.24 -    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
    7.25 +  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont ((*v) A) z"
    7.26 +    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S ((*v) A)"
    7.27    by (simp_all add: linear_continuous_at linear_continuous_on)
    7.28  
    7.29  lemma%unimportant scalar_invertible:
    7.30 @@ -293,24 +293,24 @@
    7.31  
    7.32  lemma%important norm_column_le_onorm:
    7.33    fixes A :: "real^'n^'m"
    7.34 -  shows "norm(column i A) \<le> onorm(( *v) A)"
    7.35 +  shows "norm(column i A) \<le> onorm((*v) A)"
    7.36  proof%unimportant -
    7.37    have "norm (\<chi> j. A $ j $ i) \<le> norm (A *v axis i 1)"
    7.38      by (simp add: matrix_mult_dot cart_eq_inner_axis)
    7.39 -  also have "\<dots> \<le> onorm (( *v) A)"
    7.40 +  also have "\<dots> \<le> onorm ((*v) A)"
    7.41      using onorm [OF matrix_vector_mul_bounded_linear, of A "axis i 1"] by auto
    7.42 -  finally have "norm (\<chi> j. A $ j $ i) \<le> onorm (( *v) A)" .
    7.43 +  finally have "norm (\<chi> j. A $ j $ i) \<le> onorm ((*v) A)" .
    7.44    then show ?thesis
    7.45      unfolding column_def .
    7.46  qed
    7.47  
    7.48  lemma%important matrix_component_le_onorm:
    7.49    fixes A :: "real^'n^'m"
    7.50 -  shows "\<bar>A $ i $ j\<bar> \<le> onorm(( *v) A)"
    7.51 +  shows "\<bar>A $ i $ j\<bar> \<le> onorm((*v) A)"
    7.52  proof%unimportant -
    7.53    have "\<bar>A $ i $ j\<bar> \<le> norm (\<chi> n. (A $ n $ j))"
    7.54      by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta)
    7.55 -  also have "\<dots> \<le> onorm (( *v) A)"
    7.56 +  also have "\<dots> \<le> onorm ((*v) A)"
    7.57      by (metis (no_types) column_def norm_column_le_onorm)
    7.58    finally show ?thesis .
    7.59  qed
    7.60 @@ -322,7 +322,7 @@
    7.61  
    7.62  lemma%important onorm_le_matrix_component_sum:
    7.63    fixes A :: "real^'n^'m"
    7.64 -  shows "onorm(( *v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
    7.65 +  shows "onorm((*v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
    7.66  proof%unimportant (rule onorm_le)
    7.67    fix x
    7.68    have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
    7.69 @@ -345,7 +345,7 @@
    7.70  lemma%important onorm_le_matrix_component:
    7.71    fixes A :: "real^'n^'m"
    7.72    assumes "\<And>i j. abs(A$i$j) \<le> B"
    7.73 -  shows "onorm(( *v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
    7.74 +  shows "onorm((*v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
    7.75  proof%unimportant (rule onorm_le)
    7.76    fix x :: "real^'n::_"
    7.77    have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
    7.78 @@ -403,13 +403,13 @@
    7.79      by (auto simp: lambda_skolem Bex_def)
    7.80    show ?thesis
    7.81    proof
    7.82 -    have "onorm (( *v) (A - B)) \<le> real CARD('m) * real CARD('n) *
    7.83 +    have "onorm ((*v) (A - B)) \<le> real CARD('m) * real CARD('n) *
    7.84      (e / (2 * real CARD('m) * real CARD('n)))"
    7.85        apply (rule onorm_le_matrix_component)
    7.86        using Bclo by (simp add: abs_minus_commute less_imp_le)
    7.87      also have "\<dots> < e"
    7.88        using \<open>0 < e\<close> by (simp add: divide_simps)
    7.89 -    finally show "onorm (( *v) (A - B)) < e" .
    7.90 +    finally show "onorm ((*v) (A - B)) < e" .
    7.91    qed (use B in auto)
    7.92  qed
    7.93  
    7.94 @@ -778,7 +778,7 @@
    7.95      where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
    7.96  proof%unimportant -
    7.97    from assms obtain s where "finite s"
    7.98 -    and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s"
    7.99 +    and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s"
   7.100      by (rule cube_convex_hull)
   7.101    with that[of s] show thesis
   7.102      by (simp add: const_vector_cart)
   7.103 @@ -982,11 +982,11 @@
   7.104        using basis_exists [of "span(rows A)"] by metis
   7.105      with span_subspace have eq: "span B = span(rows A)"
   7.106        by auto
   7.107 -    then have inj: "inj_on (( *v) A) (span B)"
   7.108 +    then have inj: "inj_on ((*v) A) (span B)"
   7.109        by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
   7.110 -    then have ind: "independent (( *v) A ` B)"
   7.111 +    then have ind: "independent ((*v) A ` B)"
   7.112        by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
   7.113 -    have "dim (span (rows A)) \<le> card (( *v) A ` B)"
   7.114 +    have "dim (span (rows A)) \<le> card ((*v) A ` B)"
   7.115        unfolding B(2)[symmetric]
   7.116        using inj
   7.117        by (auto simp: card_image inj_on_subset span_superset)
   7.118 @@ -1017,7 +1017,7 @@
   7.119  
   7.120  lemma%unimportant columns_image_basis:
   7.121    fixes A :: "real^'n^'m"
   7.122 -  shows "columns A = ( *v) A ` (range (\<lambda>i. axis i 1))"
   7.123 +  shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
   7.124    by (force simp: columns_def matrix_vector_mult_basis [symmetric])
   7.125  
   7.126  lemma%important rank_dim_range:
   7.127 @@ -1025,7 +1025,7 @@
   7.128    shows "rank A = dim(range (\<lambda>x. A *v x))"
   7.129    unfolding column_rank_def
   7.130  proof%unimportant (rule span_eq_dim)
   7.131 -  have "span (columns A) \<subseteq> span (range (( *v) A))" (is "?l \<subseteq> ?r")
   7.132 +  have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
   7.133      by (simp add: columns_image_basis image_subsetI span_mono)
   7.134    then show "?l = ?r"
   7.135      by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
   7.136 @@ -1040,13 +1040,13 @@
   7.137  
   7.138  lemma%unimportant full_rank_injective:
   7.139    fixes A :: "real^'n^'m"
   7.140 -  shows "rank A = CARD('n) \<longleftrightarrow> inj (( *v) A)"
   7.141 +  shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
   7.142    by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
   7.143        dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
   7.144  
   7.145  lemma%unimportant full_rank_surjective:
   7.146    fixes A :: "real^'n^'m"
   7.147 -  shows "rank A = CARD('m) \<longleftrightarrow> surj (( *v) A)"
   7.148 +  shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
   7.149    by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
   7.150                  matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
   7.151  
   7.152 @@ -1055,7 +1055,7 @@
   7.153  
   7.154  lemma%unimportant less_rank_noninjective:
   7.155    fixes A :: "real^'n^'m"
   7.156 -  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj (( *v) A)"
   7.157 +  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
   7.158  using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
   7.159  
   7.160  lemma%unimportant matrix_nonfull_linear_equations_eq:
   7.161 @@ -1071,7 +1071,7 @@
   7.162    fixes A :: "real^'n^'m" and B :: "real^'p^'n"
   7.163    shows "rank(A ** B) \<le> rank B"
   7.164  proof%unimportant -
   7.165 -  have "rank(A ** B) \<le> dim (( *v) A ` range (( *v) B))"
   7.166 +  have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
   7.167      by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
   7.168    also have "\<dots> \<le> rank B"
   7.169      by (simp add: rank_dim_range dim_image_le)
   7.170 @@ -1137,7 +1137,7 @@
   7.171  
   7.172  lemma has_derivative_vector_1:
   7.173    assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
   7.174 -  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' a))
   7.175 +  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
   7.176           (at ((vec a)::real^1) within vec ` S)"
   7.177      using der_g
   7.178      apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
     8.1 --- a/src/HOL/Analysis/Cartesian_Space.thy	Sun Sep 23 21:49:31 2018 +0200
     8.2 +++ b/src/HOL/Analysis/Cartesian_Space.thy	Mon Sep 24 14:30:09 2018 +0200
     8.3 @@ -20,7 +20,7 @@
     8.4    unfolding cart_basis_def Setcompr_eq_image
     8.5    by (rule card_image) (auto simp: inj_on_def axis_eq_axis)
     8.6  
     8.7 -interpretation vec: vector_space "( *s) "
     8.8 +interpretation vec: vector_space "(*s) "
     8.9    by unfold_locales (vector algebra_simps)+
    8.10  
    8.11  lemma%unimportant independent_cart_basis:
    8.12 @@ -90,11 +90,11 @@
    8.13  qed
    8.14  
    8.15  (*Some interpretations:*)
    8.16 -interpretation vec: finite_dimensional_vector_space "( *s)" "cart_basis"
    8.17 +interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis"
    8.18    by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis)
    8.19  
    8.20  lemma%unimportant matrix_vector_mul_linear_gen[intro, simp]:
    8.21 -  "Vector_Spaces.linear ( *s) ( *s) (( *v) A)"
    8.22 +  "Vector_Spaces.linear (*s) (*s) ((*v) A)"
    8.23    by unfold_locales
    8.24      (vector matrix_vector_mult_def sum.distrib algebra_simps)+
    8.25  
    8.26 @@ -108,10 +108,10 @@
    8.27  
    8.28  lemma%important linear_componentwise:
    8.29    fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
    8.30 -  assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
    8.31 +  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
    8.32    shows "(f x)$j = sum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
    8.33  proof%unimportant -
    8.34 -  interpret lf: Vector_Spaces.linear "( *s)" "( *s)" f
    8.35 +  interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f
    8.36      using lf .
    8.37    let ?M = "(UNIV :: 'm set)"
    8.38    let ?N = "(UNIV :: 'n set)"
    8.39 @@ -123,13 +123,13 @@
    8.40      unfolding basis_expansion by auto
    8.41  qed
    8.42  
    8.43 -interpretation vec: Vector_Spaces.linear "( *s)" "( *s)" "( *v) A"
    8.44 +interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A"
    8.45    using matrix_vector_mul_linear_gen.
    8.46  
    8.47 -interpretation vec: finite_dimensional_vector_space_pair "( *s)" cart_basis "( *s)" cart_basis ..
    8.48 +interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis ..
    8.49  
    8.50  lemma%unimportant matrix_works:
    8.51 -  assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
    8.52 +  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
    8.53    shows "matrix f *v x = f (x::'a::field ^ 'n)"
    8.54    apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
    8.55    apply clarify
    8.56 @@ -140,8 +140,8 @@
    8.57    by (simp add: matrix_eq matrix_works)
    8.58  
    8.59  lemma%unimportant matrix_compose_gen:
    8.60 -  assumes lf: "Vector_Spaces.linear ( *s) ( *s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
    8.61 -    and lg: "Vector_Spaces.linear ( *s) ( *s) (g::'a^'m \<Rightarrow> 'a^_)"
    8.62 +  assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
    8.63 +    and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \<Rightarrow> 'a^_)"
    8.64    shows "matrix (g o f) = matrix g ** matrix f"
    8.65    using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]]
    8.66    by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
    8.67 @@ -161,11 +161,11 @@
    8.68    by (metis matrix_transpose_mul transpose_mat transpose_transpose)
    8.69  
    8.70  lemma%unimportant linear_matrix_vector_mul_eq:
    8.71 -  "Vector_Spaces.linear ( *s) ( *s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
    8.72 +  "Vector_Spaces.linear (*s) (*s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
    8.73    by (simp add: scalar_mult_eq_scaleR linear_def)
    8.74  
    8.75  lemma%unimportant matrix_vector_mul[simp]:
    8.76 -  "Vector_Spaces.linear ( *s) ( *s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
    8.77 +  "Vector_Spaces.linear (*s) (*s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
    8.78    "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
    8.79    "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
    8.80    for f :: "real^'n \<Rightarrow> real ^'m"
    8.81 @@ -173,20 +173,20 @@
    8.82  
    8.83  lemma%important matrix_left_invertible_injective:
    8.84    fixes A :: "'a::field^'n^'m"
    8.85 -  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
    8.86 +  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj ((*v) A)"
    8.87  proof%unimportant safe
    8.88    fix B
    8.89    assume B: "B ** A = mat 1"
    8.90 -  show "inj (( *v) A)"
    8.91 +  show "inj ((*v) A)"
    8.92      unfolding inj_on_def
    8.93        by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
    8.94  next
    8.95 -  assume "inj (( *v) A)"
    8.96 +  assume "inj ((*v) A)"
    8.97    from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
    8.98 -  obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \<circ> ( *v) A = id"
    8.99 +  obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
   8.100      by blast
   8.101    have "matrix g ** A = mat 1"
   8.102 -    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear ( *s) ( *s) g\<close> g matrix_compose_gen
   8.103 +    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
   8.104          matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
   8.105    then show "\<exists>B. B ** A = mat 1"
   8.106      by metis
   8.107 @@ -206,11 +206,11 @@
   8.108      { fix x :: "'a ^ 'm"
   8.109        have "A *v (B *v x) = x"
   8.110          by (simp add: matrix_vector_mul_assoc AB) }
   8.111 -    hence "surj (( *v) A)" unfolding surj_def by metis }
   8.112 +    hence "surj ((*v) A)" unfolding surj_def by metis }
   8.113    moreover
   8.114 -  { assume sf: "surj (( *v) A)"
   8.115 +  { assume sf: "surj ((*v) A)"
   8.116      from vec.linear_surjective_right_inverse[OF _ this]
   8.117 -    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \<circ> g = id"
   8.118 +    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
   8.119        by blast
   8.120  
   8.121      have "A ** (matrix g) = mat 1"
   8.122 @@ -339,11 +339,11 @@
   8.123  proof%unimportant -
   8.124    { fix A A' :: "'a ^'n^'n"
   8.125      assume AA': "A ** A' = mat 1"
   8.126 -    have sA: "surj (( *v) A)"
   8.127 +    have sA: "surj ((*v) A)"
   8.128        using AA' matrix_right_invertible_surjective by auto
   8.129      from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
   8.130      obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
   8.131 -      where f': "Vector_Spaces.linear ( *s) ( *s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
   8.132 +      where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
   8.133      have th: "matrix f' ** A = mat 1"
   8.134        by (simp add: matrix_eq matrix_works[OF f'(1)]
   8.135            matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
   8.136 @@ -448,13 +448,13 @@
   8.137    finally show ?thesis .
   8.138  qed
   8.139  
   8.140 -interpretation vector_space_over_itself: vector_space "( *) :: 'a::field => 'a => 'a"
   8.141 +interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a"
   8.142    by unfold_locales (simp_all add: algebra_simps)
   8.143  
   8.144  lemmas [simp del] = vector_space_over_itself.scale_scale
   8.145  
   8.146  interpretation vector_space_over_itself: finite_dimensional_vector_space
   8.147 -  "( *) :: 'a::field => 'a => 'a" "{1}"
   8.148 +  "(*) :: 'a::field => 'a => 'a" "{1}"
   8.149    by unfold_locales (auto simp: vector_space_over_itself.span_singleton)
   8.150  
   8.151  lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
     9.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Sep 23 21:49:31 2018 +0200
     9.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Sep 24 14:30:09 2018 +0200
     9.3 @@ -228,7 +228,7 @@
     9.4  
     9.5  lemma continuous_on_joinpaths_D1:
     9.6      "continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1"
     9.7 -  apply (rule continuous_on_eq [of _ "(g1 +++ g2) \<circ> (( *)(inverse 2))"])
     9.8 +  apply (rule continuous_on_eq [of _ "(g1 +++ g2) \<circ> ((*)(inverse 2))"])
     9.9    apply (rule continuous_intros | simp)+
    9.10    apply (auto elim!: continuous_on_subset simp: joinpaths_def)
    9.11    done
    9.12 @@ -251,13 +251,13 @@
    9.13    show ?thesis
    9.14      unfolding piecewise_differentiable_on_def
    9.15    proof (intro exI conjI ballI cont)
    9.16 -    show "finite (insert 1 ((( *)2) ` S))"
    9.17 +    show "finite (insert 1 (((*)2) ` S))"
    9.18        by (simp add: \<open>finite S\<close>)
    9.19 -    show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
    9.20 +    show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
    9.21      proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
    9.22        have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}"
    9.23          by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
    9.24 -      then show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x within {0..1}"
    9.25 +      then show "g1 +++ g2 \<circ> (*) (inverse 2) differentiable at x within {0..1}"
    9.26          by (auto intro: differentiable_chain_within)
    9.27      qed (use that in \<open>auto simp: joinpaths_def\<close>)
    9.28    qed
    9.29 @@ -598,49 +598,49 @@
    9.30               and co12: "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
    9.31               and g12D: "\<forall>x\<in>{0..1} - S. g1 +++ g2 differentiable at x"
    9.32      using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    9.33 -  have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
    9.34 +  have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
    9.35    proof (rule differentiable_transform_within)
    9.36 -    show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x"
    9.37 +    show "g1 +++ g2 \<circ> (*) (inverse 2) differentiable at x"
    9.38        using that g12D
    9.39        apply (simp only: joinpaths_def)
    9.40        by (rule differentiable_chain_at derivative_intros | force)+
    9.41      show "\<And>x'. \<lbrakk>dist x' x < dist (x/2) (1/2)\<rbrakk>
    9.42 -          \<Longrightarrow> (g1 +++ g2 \<circ> ( *) (inverse 2)) x' = g1 x'"
    9.43 +          \<Longrightarrow> (g1 +++ g2 \<circ> (*) (inverse 2)) x' = g1 x'"
    9.44        using that by (auto simp: dist_real_def joinpaths_def)
    9.45    qed (use that in \<open>auto simp: dist_real_def\<close>)
    9.46 -  have [simp]: "vector_derivative (g1 \<circ> ( *) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
    9.47 -               if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
    9.48 +  have [simp]: "vector_derivative (g1 \<circ> (*) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
    9.49 +               if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
    9.50      apply (subst vector_derivative_chain_at)
    9.51      using that
    9.52      apply (rule derivative_eq_intros g1D | simp)+
    9.53      done
    9.54    have "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
    9.55      using co12 by (rule continuous_on_subset) force
    9.56 -  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 \<circ> ( *)2) (at x))"
    9.57 +  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 \<circ> (*)2) (at x))"
    9.58    proof (rule continuous_on_eq [OF _ vector_derivative_at])
    9.59 -    show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \<circ> ( *) 2) (at x)) (at x)"
    9.60 +    show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \<circ> (*) 2) (at x)) (at x)"
    9.61        if "x \<in> {0..1/2} - insert (1/2) S" for x
    9.62      proof (rule has_vector_derivative_transform_within)
    9.63 -      show "(g1 \<circ> ( *) 2 has_vector_derivative vector_derivative (g1 \<circ> ( *) 2) (at x)) (at x)"
    9.64 +      show "(g1 \<circ> (*) 2 has_vector_derivative vector_derivative (g1 \<circ> (*) 2) (at x)) (at x)"
    9.65          using that
    9.66          by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric])
    9.67 -      show "\<And>x'. \<lbrakk>dist x' x < dist x (1/2)\<rbrakk> \<Longrightarrow> (g1 \<circ> ( *) 2) x' = (g1 +++ g2) x'"
    9.68 +      show "\<And>x'. \<lbrakk>dist x' x < dist x (1/2)\<rbrakk> \<Longrightarrow> (g1 \<circ> (*) 2) x' = (g1 +++ g2) x'"
    9.69          using that by (auto simp: dist_norm joinpaths_def)
    9.70      qed (use that in \<open>auto simp: dist_norm\<close>)
    9.71    qed
    9.72 -  have "continuous_on ({0..1} - insert 1 (( *) 2 ` S))
    9.73 -                      ((\<lambda>x. 1/2 * vector_derivative (g1 \<circ> ( *)2) (at x)) \<circ> ( *)(1/2))"
    9.74 +  have "continuous_on ({0..1} - insert 1 ((*) 2 ` S))
    9.75 +                      ((\<lambda>x. 1/2 * vector_derivative (g1 \<circ> (*)2) (at x)) \<circ> (*)(1/2))"
    9.76      apply (rule continuous_intros)+
    9.77      using coDhalf
    9.78      apply (simp add: scaleR_conv_of_real image_set_diff image_image)
    9.79      done
    9.80 -  then have con_g1: "continuous_on ({0..1} - insert 1 (( *) 2 ` S)) (\<lambda>x. vector_derivative g1 (at x))"
    9.81 +  then have con_g1: "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) (\<lambda>x. vector_derivative g1 (at x))"
    9.82      by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
    9.83    have "continuous_on {0..1} g1"
    9.84      using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
    9.85    with \<open>finite S\<close> show ?thesis
    9.86      apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    9.87 -    apply (rule_tac x="insert 1 ((( *)2)`S)" in exI)
    9.88 +    apply (rule_tac x="insert 1 (((*)2)`S)" in exI)
    9.89      apply (simp add: g1D con_g1)
    9.90    done
    9.91  qed
    9.92 @@ -959,7 +959,7 @@
    9.93      apply (rule piecewise_C1_differentiable_compose)
    9.94      using assms
    9.95      apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
    9.96 -    apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
    9.97 +    apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
    9.98      done
    9.99    moreover have "(g2 \<circ> (\<lambda>x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
   9.100      apply (rule piecewise_C1_differentiable_compose)
   9.101 @@ -1030,9 +1030,9 @@
   9.102      apply (auto simp: algebra_simps vector_derivative_works)
   9.103      done
   9.104    have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
   9.105 -    apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (( *)2 -` s1)"])
   9.106 +    apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) ((*)2 -` s1)"])
   9.107      using s1
   9.108 -    apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
   9.109 +    apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
   9.110      apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
   9.111      done
   9.112    moreover have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
   9.113 @@ -1608,7 +1608,7 @@
   9.114        by (simp add: has_vector_derivative_def scaleR_conv_of_real)
   9.115      have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
   9.116        using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
   9.117 -    then have fdiff: "(f has_derivative ( *) (f' (g x))) (at (g x) within g ` {a..b})"
   9.118 +    then have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {a..b})"
   9.119        by (simp add: has_field_derivative_def)
   9.120      have "((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})"
   9.121        using diff_chain_within [OF gdiff fdiff]
   9.122 @@ -6158,9 +6158,9 @@
   9.123    case 0 then show ?case by simp
   9.124  next
   9.125    case (Suc n z)
   9.126 -  have holo0: "f holomorphic_on ( *) u ` S"
   9.127 +  have holo0: "f holomorphic_on (*) u ` S"
   9.128      by (meson fg f holomorphic_on_subset image_subset_iff)
   9.129 -  have holo2: "(deriv ^^ n) f holomorphic_on ( * ) u ` S"
   9.130 +  have holo2: "(deriv ^^ n) f holomorphic_on (*) u ` S"
   9.131      by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
   9.132    have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on S"
   9.133      by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
   9.134 @@ -6182,7 +6182,7 @@
   9.135      apply (blast intro: fg)
   9.136      done
   9.137    also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
   9.138 -      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "( *) u", unfolded o_def])
   9.139 +      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "(*) u", unfolded o_def])
   9.140        apply (rule derivative_intros)
   9.141        using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv T apply blast
   9.142        apply (simp add: deriv_linear)
    10.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Sun Sep 23 21:49:31 2018 +0200
    10.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Mon Sep 24 14:30:09 2018 +0200
    10.3 @@ -186,7 +186,7 @@
    10.4  qed
    10.5  
    10.6  lemma%unimportant matrix_vector_mult_matrix_matrix_mult_compose:
    10.7 -  "( *v) (A ** B) = ( *v) A \<circ> ( *v) B"
    10.8 +  "(*v) (A ** B) = (*v) A \<circ> (*v) B"
    10.9    by (auto simp: matrix_vector_mul_assoc)
   10.10  
   10.11  lemma%unimportant induct_linear_elementary:
   10.12 @@ -199,17 +199,17 @@
   10.13      and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
   10.14    shows "P f"
   10.15  proof -
   10.16 -  have "P (( *v) A)" for A
   10.17 +  have "P ((*v) A)" for A
   10.18    proof (rule induct_matrix_elementary_alt)
   10.19      fix A B
   10.20 -    assume "P (( *v) A)" and "P (( *v) B)"
   10.21 -    then show "P (( *v) (A ** B))"
   10.22 +    assume "P ((*v) A)" and "P ((*v) B)"
   10.23 +    then show "P ((*v) (A ** B))"
   10.24        by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
   10.25            intro!: comp)
   10.26    next
   10.27      fix A :: "real^'n^'n" and i
   10.28      assume "row i A = 0"
   10.29 -    show "P (( *v) A)"
   10.30 +    show "P ((*v) A)"
   10.31        using matrix_vector_mul_linear
   10.32        by (rule zeroes[where i=i])
   10.33          (metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta)
   10.34 @@ -218,9 +218,9 @@
   10.35      assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
   10.36      have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
   10.37        by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
   10.38 -    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = (( *v) A)"
   10.39 +    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = ((*v) A)"
   10.40        by (auto simp: 0 matrix_vector_mult_def)
   10.41 -    then show "P (( *v) A)"
   10.42 +    then show "P ((*v) A)"
   10.43        using const [of "\<lambda>i. A $ i $ i"] by simp
   10.44    next
   10.45      fix m n :: "'n"
   10.46 @@ -229,9 +229,9 @@
   10.47                (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
   10.48        for i and x :: "real^'n"
   10.49        unfolding swap_def by (rule sum.cong) auto
   10.50 -    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = (( *v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
   10.51 +    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
   10.52        by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
   10.53 -    with swap [OF \<open>m \<noteq> n\<close>] show "P (( *v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
   10.54 +    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
   10.55        by (simp add: mat_def matrix_vector_mult_def)
   10.56    next
   10.57      fix m n :: "'n"
   10.58 @@ -239,10 +239,10 @@
   10.59      then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
   10.60        by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
   10.61      then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
   10.62 -               (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   10.63 +               ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   10.64        unfolding matrix_vector_mult_def of_bool_def
   10.65        by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
   10.66 -    then show "P (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   10.67 +    then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
   10.68        using idplus [OF \<open>m \<noteq> n\<close>] by simp
   10.69    qed
   10.70    then show ?thesis
   10.71 @@ -1496,21 +1496,21 @@
   10.72                  \<le> sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}"
   10.73              by (rule sum_mono) (simp add: indicator_def divide_simps)
   10.74          next
   10.75 -          have \<alpha>: "?a = (\<Sum>k \<in> ( *)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
   10.76 +          have \<alpha>: "?a = (\<Sum>k \<in> (*)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
   10.77                           k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
   10.78              by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
   10.79            have \<beta>: "sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
   10.80                     = (\<Sum>k \<in> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
   10.81                        k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
   10.82              by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
   10.83 -          have 0: "( *) 2 ` {k \<in> \<int>. P k} \<inter> (\<lambda>x. 2 * x + 1) ` {k \<in> \<int>. P k} = {}" for P :: "real \<Rightarrow> bool"
   10.84 +          have 0: "(*) 2 ` {k \<in> \<int>. P k} \<inter> (\<lambda>x. 2 * x + 1) ` {k \<in> \<int>. P k} = {}" for P :: "real \<Rightarrow> bool"
   10.85            proof -
   10.86              have "2 * i \<noteq> 2 * j + 1" for i j :: int by arith
   10.87              thus ?thesis
   10.88                unfolding Ints_def by auto (use of_int_eq_iff in fastforce)
   10.89            qed
   10.90            have "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
   10.91 -                = (\<Sum>k \<in> ( *)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
   10.92 +                = (\<Sum>k \<in> (*)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
   10.93                    k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
   10.94              unfolding \<alpha> \<beta>
   10.95              using finite_abs_int_segment [of "2 ^ (2*n)"]
   10.96 @@ -1519,7 +1519,7 @@
   10.97            proof (rule sum_mono2)
   10.98              show "finite {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
   10.99                by (rule finite_abs_int_segment)
  10.100 -            show "( *) 2 ` {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2^(2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2^(2*n)} \<subseteq> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
  10.101 +            show "(*) 2 ` {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2^(2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2^(2*n)} \<subseteq> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
  10.102                apply auto
  10.103                using one_le_power [of "2::real" "2*n"]  by linarith
  10.104              have *: "\<lbrakk>x \<in> (S \<union> T) - U; \<And>x. x \<in> S \<Longrightarrow> x \<in> U; \<And>x. x \<in> T \<Longrightarrow> x \<in> U\<rbrakk> \<Longrightarrow> P x" for S T U P
  10.105 @@ -1535,7 +1535,7 @@
  10.106              qed
  10.107              then show "0 \<le> b/2 ^ Suc n * indicator {y. b/2 ^ Suc n \<le> f y \<and> f y < (b + 1)/2 ^ Suc n} x"
  10.108                    if "b \<in> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)} -
  10.109 -                          (( *) 2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)})" for b
  10.110 +                          ((*) 2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)})" for b
  10.111                using that by (simp add: indicator_def divide_simps)
  10.112            qed
  10.113            finally show "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<le> ?b" .
  10.114 @@ -2121,8 +2121,8 @@
  10.115            moreover
  10.116            interpret linear "f' x" by fact
  10.117            have "(matrix (f' x) - B) *v w = 0" for w
  10.118 -          proof (rule lemma_partial_derivatives [of "( *v) (matrix (f' x) - B)"])
  10.119 -            show "linear (( *v) (matrix (f' x) - B))"
  10.120 +          proof (rule lemma_partial_derivatives [of "(*v) (matrix (f' x) - B)"])
  10.121 +            show "linear ((*v) (matrix (f' x) - B))"
  10.122                by (rule matrix_vector_mul_linear)
  10.123              have "((\<lambda>y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
  10.124                using tendsto_minus [OF lim_df] by (simp add: algebra_simps divide_simps)
  10.125 @@ -2141,19 +2141,19 @@
  10.126                    proof (rule eventually_sequentiallyI)
  10.127                      fix k :: "nat"
  10.128                      assume "0 \<le> k"
  10.129 -                    have "0 \<le> onorm (( *v) (A k - B))"
  10.130 +                    have "0 \<le> onorm ((*v) (A k - B))"
  10.131                        using matrix_vector_mul_bounded_linear
  10.132                        by (rule onorm_pos_le)
  10.133 -                    then show "norm (onorm (( *v) (A k - B))) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>(A k - B) $ i $ j\<bar>)"
  10.134 +                    then show "norm (onorm ((*v) (A k - B))) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>(A k - B) $ i $ j\<bar>)"
  10.135                        by (simp add: onorm_le_matrix_component_sum del: vector_minus_component)
  10.136                    qed
  10.137                  next
  10.138                    show "?g \<longlonglongrightarrow> 0"
  10.139                      using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: tendsto_null_sum)
  10.140                  qed
  10.141 -                with \<open>e > 0\<close> obtain p where "\<And>n. n \<ge> p \<Longrightarrow> \<bar>onorm (( *v) (A n - B))\<bar> < e/2"
  10.142 +                with \<open>e > 0\<close> obtain p where "\<And>n. n \<ge> p \<Longrightarrow> \<bar>onorm ((*v) (A n - B))\<bar> < e/2"
  10.143                    unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral)
  10.144 -                then have pqe2: "\<bar>onorm (( *v) (A (p + q) - B))\<bar> < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*)
  10.145 +                then have pqe2: "\<bar>onorm ((*v) (A (p + q) - B))\<bar> < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*)
  10.146                    using le_add1 by blast
  10.147                  show "\<exists>d>0. \<forall>y\<in>S. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow>
  10.148                             inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e"
  10.149 @@ -2196,12 +2196,12 @@
  10.150                  by (simp add: algebra_simps diff lin_df matrix_vector_mul_linear scalar_mult_eq_scaleR)
  10.151              qed
  10.152            qed (use x in \<open>simp; auto simp: not_less\<close>)
  10.153 -          ultimately have "f' x = ( *v) B"
  10.154 +          ultimately have "f' x = (*v) B"
  10.155              by (force simp: algebra_simps scalar_mult_eq_scaleR)
  10.156            show "matrix (f' x) $ m $ n \<le> b"
  10.157            proof (rule tendsto_upperbound [of "\<lambda>i. (A i $ m $ n)" _ sequentially])
  10.158              show "(\<lambda>i. A i $ m $ n) \<longlonglongrightarrow> matrix (f' x) $ m $ n"
  10.159 -              by (simp add: B \<open>f' x = ( *v) B\<close>)
  10.160 +              by (simp add: B \<open>f' x = (*v) B\<close>)
  10.161              show "\<forall>\<^sub>F i in sequentially. A i $ m $ n \<le> b"
  10.162                by (simp add: Ab less_eq_real_def)
  10.163            qed auto
  10.164 @@ -2214,7 +2214,7 @@
  10.165              using f [OF \<open>x \<in> S\<close>] unfolding Deriv.has_derivative_at_within Lim_within
  10.166              by (auto simp: field_simps dest: spec [of _ "e/2"])
  10.167            let ?A = "matrix(f' x) - (\<chi> i j. if i = m \<and> j = n then e / 4 else 0)"
  10.168 -          obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm(( *v) (?A - B)) < e/6"
  10.169 +          obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm((*v) (?A - B)) < e/6"
  10.170              using matrix_rational_approximation \<open>e > 0\<close>
  10.171              by (metis zero_less_divide_iff zero_less_numeral)
  10.172            show "\<exists>d>0. \<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and>
  10.173 @@ -2224,7 +2224,7 @@
  10.174                by (rule \<open>d>0\<close>)
  10.175              show "B $ m $ n < b"
  10.176              proof -
  10.177 -              have "\<bar>matrix (( *v) (?A - B)) $ m $ n\<bar> \<le> onorm (( *v) (?A - B))"
  10.178 +              have "\<bar>matrix ((*v) (?A - B)) $ m $ n\<bar> \<le> onorm ((*v) (?A - B))"
  10.179                  using component_le_onorm [OF matrix_vector_mul_linear, of _ m n] by metis
  10.180                then show ?thesis
  10.181                  using b Bo_e6 by simp
  10.182 @@ -3805,12 +3805,12 @@
  10.183    let ?drop = "(\<lambda>x::real^1. x $ 1)"
  10.184    have S': "?lift ` S \<in> sets lebesgue"
  10.185      by (auto intro: differentiable_image_in_sets_lebesgue [OF S] differentiable_vec)
  10.186 -  have "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' z)) (at (vec z) within ?lift ` S)"
  10.187 +  have "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' z)) (at (vec z) within ?lift ` S)"
  10.188      if "z \<in> S" for z
  10.189      using der_g [OF that]
  10.190      by (simp add: has_vector_derivative_def has_derivative_vector_1)
  10.191    then have der': "\<And>x. x \<in> ?lift ` S \<Longrightarrow>
  10.192 -        (?lift \<circ> g \<circ> ?drop has_derivative ( *\<^sub>R) (g' (?drop x))) (at x within ?lift ` S)"
  10.193 +        (?lift \<circ> g \<circ> ?drop has_derivative (*\<^sub>R) (g' (?drop x))) (at x within ?lift ` S)"
  10.194      by (auto simp: o_def)
  10.195    have inj': "inj_on (vec \<circ> g \<circ> ?drop) (vec ` S)"
  10.196      using inj by (simp add: inj_on_def)
    11.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Sep 23 21:49:31 2018 +0200
    11.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Sep 24 14:30:09 2018 +0200
    11.3 @@ -16,7 +16,7 @@
    11.4  
    11.5  lemma has_derivative_mult_right:
    11.6    fixes c:: "'a :: real_normed_algebra"
    11.7 -  shows "((( * ) c) has_derivative (( * ) c)) F"
    11.8 +  shows "(((*) c) has_derivative ((*) c)) F"
    11.9  by (rule has_derivative_mult_right [OF has_derivative_ident])
   11.10  
   11.11  lemma has_derivative_of_real[derivative_intros, simp]:
   11.12 @@ -25,7 +25,7 @@
   11.13  
   11.14  lemma has_vector_derivative_real_field:
   11.15    "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
   11.16 -  using has_derivative_compose[of of_real of_real a _ f "( * ) f'"]
   11.17 +  using has_derivative_compose[of of_real of_real a _ f "(*) f'"]
   11.18    by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
   11.19  lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
   11.20  
   11.21 @@ -59,10 +59,10 @@
   11.22    shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
   11.23    using assms by (intro vector_derivative_cnj_within) auto
   11.24  
   11.25 -lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
   11.26 +lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
   11.27    by auto
   11.28  
   11.29 -lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
   11.30 +lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
   11.31    by auto
   11.32  
   11.33  lemma uniformly_continuous_on_cmul_right [continuous_intros]:
   11.34 @@ -283,7 +283,7 @@
   11.35  lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
   11.36    by (metis holomorphic_transform)
   11.37  
   11.38 -lemma holomorphic_on_linear [simp, holomorphic_intros]: "(( * ) c) holomorphic_on s"
   11.39 +lemma holomorphic_on_linear [simp, holomorphic_intros]: "((*) c) holomorphic_on s"
   11.40    unfolding holomorphic_on_def by (metis field_differentiable_linear)
   11.41  
   11.42  lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
   11.43 @@ -572,7 +572,7 @@
   11.44    finally show ?thesis .
   11.45  qed
   11.46  
   11.47 -lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on S"
   11.48 +lemma analytic_on_linear [analytic_intros,simp]: "((*) c) analytic_on S"
   11.49    by (auto simp add: analytic_on_holomorphic)
   11.50  
   11.51  lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on S"
   11.52 @@ -905,9 +905,9 @@
   11.53      by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
   11.54    then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   11.55      "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
   11.56 -  from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
   11.57 +  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
   11.58      by (simp add: has_field_derivative_def S)
   11.59 -  have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
   11.60 +  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
   11.61      by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
   11.62         (insert g, auto simp: sums_iff)
   11.63    thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
    12.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Sep 23 21:49:31 2018 +0200
    12.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Sep 24 14:30:09 2018 +0200
    12.3 @@ -1133,10 +1133,10 @@
    12.4        done
    12.5      with \<open>e>0\<close> show ?thesis by force
    12.6    qed
    12.7 -  have "inj (( * ) (deriv f \<xi>))"
    12.8 +  have "inj ((*) (deriv f \<xi>))"
    12.9      using dnz by simp
   12.10 -  then obtain g' where g': "linear g'" "g' \<circ> ( * ) (deriv f \<xi>) = id"
   12.11 -    using linear_injective_left_inverse [of "( * ) (deriv f \<xi>)"]
   12.12 +  then obtain g' where g': "linear g'" "g' \<circ> (*) (deriv f \<xi>) = id"
   12.13 +    using linear_injective_left_inverse [of "(*) (deriv f \<xi>)"]
   12.14      by (auto simp: linear_times)
   12.15    show ?thesis
   12.16      apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g'])
   12.17 @@ -2083,10 +2083,10 @@
   12.18      apply (simp add: C_def False fo)
   12.19      apply (simp add: derivative_intros dfa complex_derivative_chain)
   12.20      done
   12.21 -  have sb1: "( * ) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
   12.22 +  have sb1: "(*) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
   12.23               \<subseteq> f ` ball a r"
   12.24      using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
   12.25 -  have sb2: "ball (C * r * b) r' \<subseteq> ( * ) (C * r) ` ball b t"
   12.26 +  have sb2: "ball (C * r * b) r' \<subseteq> (*) (C * r) ` ball b t"
   12.27               if "1 / 12 < t" for b t
   12.28    proof -
   12.29      have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
    13.1 --- a/src/HOL/Analysis/Connected.thy	Sun Sep 23 21:49:31 2018 +0200
    13.2 +++ b/src/HOL/Analysis/Connected.thy	Mon Sep 24 14:30:09 2018 +0200
    13.3 @@ -2257,14 +2257,14 @@
    13.4          unfolding dist_norm
    13.5          using norm_scaleR[of c "(1 / c) *\<^sub>R y - x", unfolded scaleR_right_diff_distrib, unfolded scaleR_scaleR] assms(1)
    13.6            assms(1)[unfolded zero_less_abs_iff[symmetric]] by (simp del:zero_less_abs_iff)
    13.7 -      then have "y \<in> ( *\<^sub>R) c ` s"
    13.8 -        using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "( *\<^sub>R) c"]
    13.9 +      then have "y \<in> (*\<^sub>R) c ` s"
   13.10 +        using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "(*\<^sub>R) c"]
   13.11          using e[THEN spec[where x="(1 / c) *\<^sub>R y"]]
   13.12          using assms(1)
   13.13          unfolding dist_norm scaleR_scaleR
   13.14          by auto
   13.15      }
   13.16 -    ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> ( *\<^sub>R) c ` s"
   13.17 +    ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> (*\<^sub>R) c ` s"
   13.18        apply (rule_tac x="e * \<bar>c\<bar>" in exI, auto)
   13.19        done
   13.20    }
   13.21 @@ -2311,10 +2311,10 @@
   13.22  proof -
   13.23    have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)"
   13.24      unfolding o_def ..
   13.25 -  have "(+) a ` ( *\<^sub>R) c ` S = ((+) a \<circ> ( *\<^sub>R) c) ` S"
   13.26 +  have "(+) a ` (*\<^sub>R) c ` S = ((+) a \<circ> (*\<^sub>R) c) ` S"
   13.27      by auto
   13.28    then show ?thesis
   13.29 -    using assms open_translation[of "( *\<^sub>R) c ` S" a]
   13.30 +    using assms open_translation[of "(*\<^sub>R) c ` S" a]
   13.31      unfolding *
   13.32      by auto
   13.33  qed
   13.34 @@ -2637,7 +2637,7 @@
   13.35    assumes "compact s"
   13.36    shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
   13.37  proof -
   13.38 -  have "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
   13.39 +  have "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
   13.40      by auto
   13.41    then show ?thesis
   13.42      using compact_translation[OF compact_scaling[OF assms], of a c] by auto
   13.43 @@ -3719,7 +3719,7 @@
   13.44    assumes "c \<noteq> 0"
   13.45    shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
   13.46  proof -
   13.47 -  have *: "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
   13.48 +  have *: "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
   13.49    show ?thesis
   13.50      using homeomorphic_trans
   13.51      using homeomorphic_scaling[OF assms, of s]
    14.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Sep 23 21:49:31 2018 +0200
    14.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Sep 24 14:30:09 2018 +0200
    14.3 @@ -664,7 +664,7 @@
    14.4    assumes "convex S"
    14.5    shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)"
    14.6  proof -
    14.7 -  have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` ( *\<^sub>R) c ` S"
    14.8 +  have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S"
    14.9      by auto
   14.10    then show ?thesis
   14.11      using convex_translation[OF convex_scaling[OF assms], of a c] by auto
   14.12 @@ -1229,12 +1229,12 @@
   14.13  
   14.14  lemma closure_scaleR:
   14.15    fixes S :: "'a::real_normed_vector set"
   14.16 -  shows "(( *\<^sub>R) c) ` (closure S) = closure ((( *\<^sub>R) c) ` S)"
   14.17 +  shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
   14.18  proof
   14.19 -  show "(( *\<^sub>R) c) ` (closure S) \<subseteq> closure ((( *\<^sub>R) c) ` S)"
   14.20 +  show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
   14.21      using bounded_linear_scaleR_right
   14.22      by (rule closure_bounded_linear_image_subset)
   14.23 -  show "closure ((( *\<^sub>R) c) ` S) \<subseteq> (( *\<^sub>R) c) ` (closure S)"
   14.24 +  show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
   14.25      by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
   14.26  qed
   14.27  
   14.28 @@ -1945,7 +1945,7 @@
   14.29  
   14.30  lemma cone_iff:
   14.31    assumes "S \<noteq> {}"
   14.32 -  shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
   14.33 +  shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
   14.34  proof -
   14.35    {
   14.36      assume "cone S"
   14.37 @@ -1955,7 +1955,7 @@
   14.38        {
   14.39          fix x
   14.40          assume "x \<in> S"
   14.41 -        then have "x \<in> (( *\<^sub>R) c) ` S"
   14.42 +        then have "x \<in> ((*\<^sub>R) c) ` S"
   14.43            unfolding image_def
   14.44            using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"]
   14.45              exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
   14.46 @@ -1964,19 +1964,19 @@
   14.47        moreover
   14.48        {
   14.49          fix x
   14.50 -        assume "x \<in> (( *\<^sub>R) c) ` S"
   14.51 +        assume "x \<in> ((*\<^sub>R) c) ` S"
   14.52          then have "x \<in> S"
   14.53            using \<open>cone S\<close> \<open>c > 0\<close>
   14.54            unfolding cone_def image_def \<open>c > 0\<close> by auto
   14.55        }
   14.56 -      ultimately have "(( *\<^sub>R) c) ` S = S" by auto
   14.57 +      ultimately have "((*\<^sub>R) c) ` S = S" by auto
   14.58      }
   14.59 -    then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
   14.60 +    then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
   14.61        using \<open>cone S\<close> cone_contains_0[of S] assms by auto
   14.62    }
   14.63    moreover
   14.64    {
   14.65 -    assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
   14.66 +    assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
   14.67      {
   14.68        fix x
   14.69        assume "x \<in> S"
   14.70 @@ -2061,9 +2061,9 @@
   14.71    then show ?thesis by auto
   14.72  next
   14.73    case False
   14.74 -  then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
   14.75 +  then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
   14.76      using cone_iff[of S] assms by auto
   14.77 -  then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` closure S = closure S)"
   14.78 +  then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
   14.79      using closure_subset by (auto simp: closure_scaleR)
   14.80    then show ?thesis
   14.81      using False cone_iff[of "closure S"] by auto
   14.82 @@ -5705,19 +5705,19 @@
   14.83    then show ?thesis by auto
   14.84  next
   14.85    case False
   14.86 -  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
   14.87 +  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
   14.88      using cone_iff[of S] assms by auto
   14.89    {
   14.90      fix c :: real
   14.91      assume "c > 0"
   14.92 -    then have "( *\<^sub>R) c ` (convex hull S) = convex hull (( *\<^sub>R) c ` S)"
   14.93 +    then have "(*\<^sub>R) c ` (convex hull S) = convex hull ((*\<^sub>R) c ` S)"
   14.94        using convex_hull_scaling[of _ S] by auto
   14.95      also have "\<dots> = convex hull S"
   14.96        using * \<open>c > 0\<close> by auto
   14.97 -    finally have "( *\<^sub>R) c ` (convex hull S) = convex hull S"
   14.98 +    finally have "(*\<^sub>R) c ` (convex hull S) = convex hull S"
   14.99        by auto
  14.100    }
  14.101 -  then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> (( *\<^sub>R) c ` (convex hull S)) = (convex hull S)"
  14.102 +  then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> ((*\<^sub>R) c ` (convex hull S)) = (convex hull S)"
  14.103      using * hull_subset[of S convex] by auto
  14.104    then show ?thesis
  14.105      using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto
  14.106 @@ -6403,7 +6403,7 @@
  14.107      assume "y \<in> cbox (x - ?d) (x + ?d)"
  14.108      then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
  14.109        using assms by (simp add: mem_box field_simps inner_simps)
  14.110 -    with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
  14.111 +    with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum ((*\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
  14.112        by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
  14.113    next
  14.114      fix y
    15.1 --- a/src/HOL/Analysis/Derivative.thy	Sun Sep 23 21:49:31 2018 +0200
    15.2 +++ b/src/HOL/Analysis/Derivative.thy	Mon Sep 24 14:30:09 2018 +0200
    15.3 @@ -52,7 +52,7 @@
    15.4  lemma has_derivative_right:
    15.5    fixes f :: "real \<Rightarrow> real"
    15.6      and y :: "real"
    15.7 -  shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
    15.8 +  shows "(f has_derivative ((*) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
    15.9           ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
   15.10  proof -
   15.11    have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
   15.12 @@ -983,7 +983,7 @@
   15.13    assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
   15.14    shows   "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
   15.15  proof (rule has_derivative_zero_constant)
   15.16 -  have A: "( * ) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
   15.17 +  have A: "(*) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
   15.18    fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
   15.19      using assms(2)[of x] by (simp add: has_field_derivative_def A)
   15.20  qed fact
   15.21 @@ -1911,9 +1911,9 @@
   15.22    then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   15.23      "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
   15.24    from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
   15.25 -  from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
   15.26 +  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
   15.27      by (simp add: has_field_derivative_def S)
   15.28 -  have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
   15.29 +  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
   15.30      by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
   15.31         (insert g, auto simp: sums_iff)
   15.32    thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
   15.33 @@ -2218,7 +2218,7 @@
   15.34    unfolding field_differentiable_def
   15.35    by (metis DERIV_subset top_greatest)
   15.36  
   15.37 -lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F"
   15.38 +lemma field_differentiable_linear [simp,derivative_intros]: "((*) c) field_differentiable F"
   15.39    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
   15.40    by (force intro: has_derivative_mult_right)
   15.41  
    16.1 --- a/src/HOL/Analysis/Determinants.thy	Sun Sep 23 21:49:31 2018 +0200
    16.2 +++ b/src/HOL/Analysis/Determinants.thy	Mon Sep 24 14:30:09 2018 +0200
    16.3 @@ -452,7 +452,7 @@
    16.4  lemma%unimportant  matrix_id [simp]: "det (matrix id) = 1"
    16.5    by (simp add: matrix_id_mat_1)
    16.6  
    16.7 -lemma%important  det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
    16.8 +lemma%important  det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
    16.9    apply (subst det_diagonal)
   16.10     apply (auto simp: matrix_def mat_def)
   16.11    apply (simp add: cart_eq_inner_axis inner_axis_axis)
   16.12 @@ -750,7 +750,7 @@
   16.13  
   16.14  lemma%unimportant  det_nz_iff_inj_gen:
   16.15    fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n"
   16.16 -  assumes "Vector_Spaces.linear ( *s) ( *s) f"
   16.17 +  assumes "Vector_Spaces.linear (*s) (*s) f"
   16.18    shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
   16.19  proof
   16.20    assume "det (matrix f) \<noteq> 0"
   16.21 @@ -780,22 +780,22 @@
   16.22  
   16.23  lemma%important  matrix_left_invertible_gen:
   16.24    fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   16.25 -  assumes "Vector_Spaces.linear ( *s) ( *s) f"
   16.26 -  shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id))"
   16.27 +  assumes "Vector_Spaces.linear (*s) (*s) f"
   16.28 +  shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id))"
   16.29  proof%unimportant safe
   16.30    fix B
   16.31    assume 1: "B ** matrix f = mat 1"
   16.32 -  show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
   16.33 +  show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id"
   16.34    proof (intro exI conjI)
   16.35 -    show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)"
   16.36 +    show "Vector_Spaces.linear (*s) (*s) (\<lambda>y. B *v y)"
   16.37        by simp
   16.38 -    show "(( *v) B) \<circ> f = id"
   16.39 +    show "((*v) B) \<circ> f = id"
   16.40        unfolding o_def
   16.41        by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid)
   16.42    qed
   16.43  next
   16.44    fix g
   16.45 -  assume "Vector_Spaces.linear ( *s) ( *s) g" "g \<circ> f = id"
   16.46 +  assume "Vector_Spaces.linear (*s) (*s) g" "g \<circ> f = id"
   16.47    then have "matrix g ** matrix f = mat 1"
   16.48      by (metis assms matrix_compose_gen matrix_id_mat_1)
   16.49    then show "\<exists>B. B ** matrix f = mat 1" ..
   16.50 @@ -808,22 +808,22 @@
   16.51  
   16.52  lemma%unimportant  matrix_right_invertible_gen:
   16.53    fixes f :: "'a::field^'m \<Rightarrow> 'a^'n"
   16.54 -  assumes "Vector_Spaces.linear ( *s) ( *s) f"
   16.55 -  shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id))"
   16.56 +  assumes "Vector_Spaces.linear (*s) (*s) f"
   16.57 +  shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id))"
   16.58  proof safe
   16.59    fix B
   16.60    assume 1: "matrix f ** B = mat 1"
   16.61 -  show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id"
   16.62 +  show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id"
   16.63    proof (intro exI conjI)
   16.64 -    show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)"
   16.65 +    show "Vector_Spaces.linear (*s) (*s) ((*v) B)"
   16.66        by simp
   16.67 -    show "f \<circ> ( *v) B = id"
   16.68 +    show "f \<circ> (*v) B = id"
   16.69        using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
   16.70        by (metis (no_types, hide_lams))
   16.71    qed
   16.72  next
   16.73    fix g
   16.74 -  assume "Vector_Spaces.linear ( *s) ( *s) g" and "f \<circ> g = id"
   16.75 +  assume "Vector_Spaces.linear (*s) (*s) g" and "f \<circ> g = id"
   16.76    then have "matrix f ** matrix g = mat 1"
   16.77      by (metis assms matrix_compose_gen matrix_id_mat_1)
   16.78    then show "\<exists>B. matrix f ** B = mat 1" ..
   16.79 @@ -836,8 +836,8 @@
   16.80  
   16.81  lemma%unimportant  matrix_invertible_gen:
   16.82    fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   16.83 -  assumes "Vector_Spaces.linear ( *s) ( *s) f"
   16.84 -  shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
   16.85 +  assumes "Vector_Spaces.linear (*s) (*s) f"
   16.86 +  shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
   16.87      (is "?lhs = ?rhs")
   16.88  proof
   16.89    assume ?lhs then show ?rhs
   16.90 @@ -855,7 +855,7 @@
   16.91  
   16.92  lemma%unimportant  invertible_eq_bij:
   16.93    fixes m :: "'a::field^'m^'n"
   16.94 -  shows "invertible m \<longleftrightarrow> bij (( *v) m)"
   16.95 +  shows "invertible m \<longleftrightarrow> bij ((*v) m)"
   16.96    using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul]
   16.97    by (metis bij_betw_def left_right_inverse_eq matrix_vector_mul_linear_gen o_bij
   16.98        vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
   16.99 @@ -1028,7 +1028,7 @@
  16.100    let ?m1 = "mat 1 :: real ^'n^'n"
  16.101    {
  16.102      assume ot: ?ot
  16.103 -    from ot have lf: "Vector_Spaces.linear ( *s) ( *s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
  16.104 +    from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
  16.105        unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR
  16.106        by blast+
  16.107      {
  16.108 @@ -1052,7 +1052,7 @@
  16.109    }
  16.110    moreover
  16.111    {
  16.112 -    assume lf: "Vector_Spaces.linear ( *s) ( *s) f" and om: "orthogonal_matrix ?mf"
  16.113 +    assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
  16.114      from lf om have ?lhs
  16.115        unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
  16.116        apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
    17.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Sun Sep 23 21:49:31 2018 +0200
    17.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Mon Sep 24 14:30:09 2018 +0200
    17.3 @@ -307,7 +307,7 @@
    17.4  subsection \<open>Locale instances\<close>
    17.5  
    17.6  lemma finite_dimensional_vector_space_euclidean:
    17.7 -  "finite_dimensional_vector_space ( *\<^sub>R) Basis"
    17.8 +  "finite_dimensional_vector_space (*\<^sub>R) Basis"
    17.9  proof unfold_locales
   17.10    show "finite (Basis::'a set)" by (metis finite_Basis)
   17.11    show "real_vector.independent (Basis::'a set)"
   17.12 @@ -318,20 +318,20 @@
   17.13      apply (drule_tac f="inner a" in arg_cong)
   17.14      apply (simp add: inner_Basis inner_sum_right eq_commute)
   17.15      done
   17.16 -  show "module.span ( *\<^sub>R) Basis = UNIV"
   17.17 +  show "module.span (*\<^sub>R) Basis = UNIV"
   17.18      unfolding span_finite [OF finite_Basis] span_raw_def[symmetric]
   17.19      by (auto intro!: euclidean_representation[symmetric])
   17.20  qed
   17.21  
   17.22  interpretation eucl?: finite_dimensional_vector_space "scaleR :: real => 'a => 'a::euclidean_space" "Basis"
   17.23 -  rewrites "module.dependent ( *\<^sub>R) = dependent"
   17.24 -    and "module.representation ( *\<^sub>R) = representation"
   17.25 -    and "module.subspace ( *\<^sub>R) = subspace"
   17.26 -    and "module.span ( *\<^sub>R) = span"
   17.27 -    and "vector_space.extend_basis ( *\<^sub>R) = extend_basis"
   17.28 -    and "vector_space.dim ( *\<^sub>R) = dim"
   17.29 -    and "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
   17.30 -    and "Vector_Spaces.linear ( * ) ( *\<^sub>R) = linear"
   17.31 +  rewrites "module.dependent (*\<^sub>R) = dependent"
   17.32 +    and "module.representation (*\<^sub>R) = representation"
   17.33 +    and "module.subspace (*\<^sub>R) = subspace"
   17.34 +    and "module.span (*\<^sub>R) = span"
   17.35 +    and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
   17.36 +    and "vector_space.dim (*\<^sub>R) = dim"
   17.37 +    and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
   17.38 +    and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
   17.39      and "finite_dimensional_vector_space.dimension Basis = DIM('a)"
   17.40      and "dimension = DIM('a)"
   17.41    by (auto simp add: dependent_raw_def representation_raw_def
   17.42 @@ -348,15 +348,15 @@
   17.43  
   17.44  interpretation eucl?: finite_dimensional_vector_space_prod scaleR scaleR Basis Basis
   17.45    rewrites "Basis_pair = Basis"
   17.46 -    and "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
   17.47 +    and "module_prod.scale (*\<^sub>R) (*\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
   17.48  proof -
   17.49 -  show "finite_dimensional_vector_space_prod ( *\<^sub>R) ( *\<^sub>R) Basis Basis"
   17.50 +  show "finite_dimensional_vector_space_prod (*\<^sub>R) (*\<^sub>R) Basis Basis"
   17.51      by unfold_locales
   17.52 -  interpret finite_dimensional_vector_space_prod "( *\<^sub>R)" "( *\<^sub>R)" "Basis::'a set" "Basis::'b set"
   17.53 +  interpret finite_dimensional_vector_space_prod "(*\<^sub>R)" "(*\<^sub>R)" "Basis::'a set" "Basis::'b set"
   17.54      by fact
   17.55    show "Basis_pair = Basis"
   17.56      unfolding Basis_pair_def Basis_prod_def by auto
   17.57 -  show "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = scaleR"
   17.58 +  show "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
   17.59      by (fact module_prod_scale_eq_scaleR)
   17.60  qed
   17.61  
    18.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Sep 23 21:49:31 2018 +0200
    18.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Sep 24 14:30:09 2018 +0200
    18.3 @@ -235,7 +235,7 @@
    18.4  instantiation vec :: (times, finite) times
    18.5  begin
    18.6  
    18.7 -definition "( * ) \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
    18.8 +definition "(*) \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
    18.9  instance ..
   18.10  
   18.11  end
   18.12 @@ -961,7 +961,7 @@
   18.13  lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
   18.14    by (simp add: vec_eq_iff)
   18.15  
   18.16 -lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear ( * ) vector_scalar_mult vec"
   18.17 +lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear (*) vector_scalar_mult vec"
   18.18    by unfold_locales (vector algebra_simps)+
   18.19  
   18.20  lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
   18.21 @@ -1161,7 +1161,7 @@
   18.22  lemma%unimportant matrix_id_mat_1: "matrix id = mat 1"
   18.23    by (simp add: mat_def matrix_def axis_def)
   18.24  
   18.25 -lemma%unimportant matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
   18.26 +lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
   18.27    by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
   18.28  
   18.29  lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
   18.30 @@ -1218,7 +1218,7 @@
   18.31  lemma%unimportant inj_matrix_vector_mult:
   18.32    fixes A::"'a::field^'n^'m"
   18.33    assumes "invertible A"
   18.34 -  shows "inj (( *v) A)"
   18.35 +  shows "inj ((*v) A)"
   18.36    by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
   18.37  
   18.38  lemma%important scalar_invertible:
    19.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Sun Sep 23 21:49:31 2018 +0200
    19.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Sep 24 14:30:09 2018 +0200
    19.3 @@ -929,7 +929,7 @@
    19.4        using E by (subst insert) (auto intro!: prod.cong)
    19.5      also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
    19.6         emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
    19.7 -      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="( * )"] prod.cong)
    19.8 +      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
    19.9      also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
   19.10        using insert(1,2) J E by (intro prod.mono_neutral_right) auto
   19.11      finally show "?\<mu> ?p = \<dots>" .
    20.1 --- a/src/HOL/Analysis/Further_Topology.thy	Sun Sep 23 21:49:31 2018 +0200
    20.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Mon Sep 24 14:30:09 2018 +0200
    20.3 @@ -3549,12 +3549,12 @@
    20.4        by (intro conjI contg continuous_intros)
    20.5      show "(complex_of_real \<circ> g) ` S \<subseteq> \<real>"
    20.6        by auto
    20.7 -    show "continuous_on \<real> (exp \<circ> ( * )\<i>)"
    20.8 +    show "continuous_on \<real> (exp \<circ> (*)\<i>)"
    20.9        by (intro continuous_intros)
   20.10 -    show "(exp \<circ> ( * )\<i>) ` \<real> \<subseteq> sphere 0 1"
   20.11 +    show "(exp \<circ> (*)\<i>) ` \<real> \<subseteq> sphere 0 1"
   20.12        by (auto simp: complex_is_Real_iff)
   20.13    qed (auto simp: convex_Reals convex_imp_contractible)
   20.14 -  moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> ( * )\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
   20.15 +  moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> (*)\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
   20.16      by (simp add: g)
   20.17    ultimately show ?lhs
   20.18      apply (rule_tac x=a in exI)
    21.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Sun Sep 23 21:49:31 2018 +0200
    21.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 24 14:30:09 2018 +0200
    21.3 @@ -2049,7 +2049,7 @@
    21.4  
    21.5      moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
    21.6      hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
    21.7 -      using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "( * )2" "2*z"]
    21.8 +      using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "(*)2" "2*z"]
    21.9        by (intro tendsto_intros Gamma_series'_LIMSEQ)
   21.10           (simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
   21.11      ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
   21.12 @@ -3131,10 +3131,10 @@
   21.13        case True
   21.14        have "(\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \<partial>lborel) = 
   21.15                (\<integral>\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1)) 
   21.16 -                \<partial>distr lborel borel (( * ) (1 / u)))" (is "_ = nn_integral _ ?f")
   21.17 +                \<partial>distr lborel borel ((*) (1 / u)))" (is "_ = nn_integral _ ?f")
   21.18          using True
   21.19          by (subst nn_integral_distr) (auto simp: indicator_def field_simps intro!: nn_integral_cong)
   21.20 -      also have "distr lborel borel (( * ) (1 / u)) = density lborel (\<lambda>_. u)"
   21.21 +      also have "distr lborel borel ((*) (1 / u)) = density lborel (\<lambda>_. u)"
   21.22          using \<open>u > 0\<close> by (subst lborel_distr_mult) auto
   21.23        also have "nn_integral \<dots> ?f = (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) *
   21.24                                                (u * (1 - x)) powr (b - 1))) \<partial>lborel)" using \<open>u > 0\<close>
    22.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Sun Sep 23 21:49:31 2018 +0200
    22.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Sep 24 14:30:09 2018 +0200
    22.3 @@ -225,7 +225,7 @@
    22.4      by (intro summable_Leibniz(1) decseq_imp_monoseq decseq_SucI) simp_all
    22.5    hence A: "(\<lambda>n. \<Sum>k<n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
    22.6      by (simp add: summable_sums_iff divide_inverse sums_def)
    22.7 -  from filterlim_compose[OF this filterlim_subseq[of "( * ) (2::nat)"]]
    22.8 +  from filterlim_compose[OF this filterlim_subseq[of "(*) (2::nat)"]]
    22.9      have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
   22.10      by (simp add: strict_mono_def)
   22.11    ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
    23.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Sep 23 21:49:31 2018 +0200
    23.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Sep 24 14:30:09 2018 +0200
    23.3 @@ -5044,8 +5044,8 @@
    23.4        using real_arch_simple by blast
    23.5      have "ball 0 B \<subseteq> ?cube n" if n: "n \<ge> N" for n
    23.6      proof -
    23.7 -      have "sum (( *\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
    23.8 -            x \<bullet> i \<le> sum (( *\<^sub>R) (real n)) Basis \<bullet> i"
    23.9 +      have "sum ((*\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
   23.10 +            x \<bullet> i \<le> sum ((*\<^sub>R) (real n)) Basis \<bullet> i"
   23.11          if "norm x < B" "i \<in> Basis" for x i::'n
   23.12            using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf)
   23.13        then show ?thesis
   23.14 @@ -5080,7 +5080,7 @@
   23.15          fix x :: 'n
   23.16          assume x: "x \<in> ball 0 B"
   23.17          have "\<lbrakk>norm (0 - x) < B; i \<in> Basis\<rbrakk>
   23.18 -              \<Longrightarrow> sum (( *\<^sub>R) (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum (( *\<^sub>R) n) Basis \<bullet> i" for i
   23.19 +              \<Longrightarrow> sum ((*\<^sub>R) (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum ((*\<^sub>R) n) Basis \<bullet> i" for i
   23.20            using Basis_le_norm[of i x] n by (auto simp add: field_simps sum_negf)
   23.21          then show "x \<in> ?cube n"
   23.22            using x by (auto simp: mem_box dist_norm)
   23.23 @@ -6180,7 +6180,7 @@
   23.24      and bou: "bounded (range(\<lambda>k. integral S (f k)))"
   23.25    shows "g integrable_on S \<and> (\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
   23.26  proof -
   23.27 -  have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = ( *\<^sub>R) (- 1) ` (range(\<lambda>k. integral S (f k)))"
   23.28 +  have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = (*\<^sub>R) (- 1) ` (range(\<lambda>k. integral S (f k)))"
   23.29      by force
   23.30    have "(\<lambda>x. - g x) integrable_on S \<and> (\<lambda>k. integral S (\<lambda>x. - f k x)) \<longlonglongrightarrow> integral S (\<lambda>x. - g x)"
   23.31    proof (rule monotone_convergence_increasing)
    24.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Sun Sep 23 21:49:31 2018 +0200
    24.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Sep 24 14:30:09 2018 +0200
    24.3 @@ -835,9 +835,9 @@
    24.4    have "((sphere a r \<inter> T) - {b}) homeomorphic
    24.5          (+) (-a) ` ((sphere a r \<inter> T) - {b})"
    24.6      by (rule homeomorphic_translation)
    24.7 -  also have "... homeomorphic ( *\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
    24.8 +  also have "... homeomorphic (*\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
    24.9      by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
   24.10 -  also have "... = sphere 0 1 \<inter> (( *\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
   24.11 +  also have "... = sphere 0 1 \<inter> ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
   24.12      using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
   24.13    also have "... homeomorphic p"
   24.14      apply (rule homeomorphic_punctured_affine_sphere_affine_01)
   24.15 @@ -2210,26 +2210,26 @@
   24.16                  and pq'_eq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p (q' t) = (f \<circ> g +++ reversepath g') t"
   24.17          using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] \<open>path q\<close> piq refl refl]
   24.18          by auto
   24.19 -      have "q' t = (h \<circ> ( *\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
   24.20 -      proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> ( *\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> ( *\<^sub>R) 2" t])
   24.21 -        show "q' 0 = (h \<circ> ( *\<^sub>R) 2) 0"
   24.22 +      have "q' t = (h \<circ> (*\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
   24.23 +      proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> (*\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> (*\<^sub>R) 2" t])
   24.24 +        show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
   24.25            by (metis \<open>pathstart q' = pathstart q\<close> comp_def g h pastq pathstart_def pth_4(2))
   24.26 -        show "continuous_on {0..1/2} (f \<circ> g \<circ> ( *\<^sub>R) 2)"
   24.27 +        show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
   24.28            apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
   24.29            using g(2) path_image_def by fastforce+
   24.30 -        show "(f \<circ> g \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
   24.31 +        show "(f \<circ> g \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
   24.32            using g(2) path_image_def fim by fastforce
   24.33 -        show "(h \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
   24.34 +        show "(h \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
   24.35            using h path_image_def by fastforce
   24.36          show "q' ` {0..1/2} \<subseteq> C"
   24.37            using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
   24.38 -        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p (q' x)"
   24.39 +        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p (q' x)"
   24.40            by (auto simp: joinpaths_def pq'_eq)
   24.41 -        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p ((h \<circ> ( *\<^sub>R) 2) x)"
   24.42 +        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p ((h \<circ> (*\<^sub>R) 2) x)"
   24.43            by (simp add: phg)
   24.44          show "continuous_on {0..1/2} q'"
   24.45            by (simp add: continuous_on_path \<open>path q'\<close>)
   24.46 -        show "continuous_on {0..1/2} (h \<circ> ( *\<^sub>R) 2)"
   24.47 +        show "continuous_on {0..1/2} (h \<circ> (*\<^sub>R) 2)"
   24.48            apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path h\<close>], force)
   24.49            done
   24.50        qed (use that in auto)
    25.1 --- a/src/HOL/Analysis/Inner_Product.thy	Sun Sep 23 21:49:31 2018 +0200
    25.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Mon Sep 24 14:30:09 2018 +0200
    25.3 @@ -277,7 +277,7 @@
    25.4  instantiation real :: real_inner
    25.5  begin
    25.6  
    25.7 -definition inner_real_def [simp]: "inner = ( * )"
    25.8 +definition inner_real_def [simp]: "inner = (*)"
    25.9  
   25.10  instance
   25.11  proof
    26.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Sep 23 21:49:31 2018 +0200
    26.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Sep 24 14:30:09 2018 +0200
    26.3 @@ -767,10 +767,10 @@
    26.4    finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
    26.5  qed
    26.6  
    26.7 -lemma lebesgue_measurable_scaling[measurable]: "( *\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
    26.8 +lemma lebesgue_measurable_scaling[measurable]: "(*\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
    26.9  proof cases
   26.10    assume "x = 0"
   26.11 -  then have "( *\<^sub>R) x = (\<lambda>x. 0::'a)"
   26.12 +  then have "(*\<^sub>R) x = (\<lambda>x. 0::'a)"
   26.13      by (auto simp: fun_eq_iff)
   26.14    then show ?thesis by auto
   26.15  next
   26.16 @@ -860,9 +860,9 @@
   26.17  
   26.18  lemma lborel_distr_mult:
   26.19    assumes "(c::real) \<noteq> 0"
   26.20 -  shows "distr lborel borel (( * ) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
   26.21 +  shows "distr lborel borel ((*) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
   26.22  proof-
   26.23 -  have "distr lborel borel (( * ) c) = distr lborel lborel (( * ) c)" by (simp cong: distr_cong)
   26.24 +  have "distr lborel borel ((*) c) = distr lborel lborel ((*) c)" by (simp cong: distr_cong)
   26.25    also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
   26.26      by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
   26.27    finally show ?thesis .
   26.28 @@ -870,13 +870,13 @@
   26.29  
   26.30  lemma lborel_distr_mult':
   26.31    assumes "(c::real) \<noteq> 0"
   26.32 -  shows "lborel = density (distr lborel borel (( * ) c)) (\<lambda>_. \<bar>c\<bar>)"
   26.33 +  shows "lborel = density (distr lborel borel ((*) c)) (\<lambda>_. \<bar>c\<bar>)"
   26.34  proof-
   26.35    have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
   26.36    also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp
   26.37    also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)"
   26.38      by (subst density_density_eq) (auto simp: ennreal_mult)
   26.39 -  also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (( * ) c)"
   26.40 +  also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel ((*) c)"
   26.41      by (rule lborel_distr_mult[symmetric])
   26.42    finally show ?thesis .
   26.43  qed
   26.44 @@ -1119,7 +1119,7 @@
   26.45  
   26.46    let ?f = "\<lambda>n. root DIM('a) (Suc n)"
   26.47  
   26.48 -  have vimage_eq_image: "( *\<^sub>R) (?f n) -` S = ( *\<^sub>R) (1 / ?f n) ` S" for n
   26.49 +  have vimage_eq_image: "(*\<^sub>R) (?f n) -` S = (*\<^sub>R) (1 / ?f n) ` S" for n
   26.50      apply safe
   26.51      subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
   26.52      subgoal by auto
   26.53 @@ -1141,20 +1141,20 @@
   26.54      by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide)
   26.55    then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)"
   26.56      unfolding ennreal_suminf_multc eq by simp
   26.57 -  also have "\<dots> = (\<Sum>n. emeasure lebesgue (( *\<^sub>R) (?f n) -` S))"
   26.58 +  also have "\<dots> = (\<Sum>n. emeasure lebesgue ((*\<^sub>R) (?f n) -` S))"
   26.59      unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp
   26.60 -  also have "\<dots> = emeasure lebesgue (\<Union>n. ( *\<^sub>R) (?f n) -` S)"
   26.61 +  also have "\<dots> = emeasure lebesgue (\<Union>n. (*\<^sub>R) (?f n) -` S)"
   26.62    proof (intro suminf_emeasure)
   26.63 -    show "disjoint_family (\<lambda>n. ( *\<^sub>R) (?f n) -` S)"
   26.64 +    show "disjoint_family (\<lambda>n. (*\<^sub>R) (?f n) -` S)"
   26.65        unfolding disjoint_family_on_def
   26.66      proof safe
   26.67        fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S"
   26.68        with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}"
   26.69          by auto
   26.70      qed
   26.71 -    have "( *\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
   26.72 +    have "(*\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
   26.73        using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto
   26.74 -    then show "range (\<lambda>i. ( *\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
   26.75 +    then show "range (\<lambda>i. (*\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
   26.76        by auto
   26.77    qed
   26.78    also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)"
    27.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Sep 23 21:49:31 2018 +0200
    27.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Sep 24 14:30:09 2018 +0200
    27.3 @@ -279,7 +279,7 @@
    27.4  lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="(+)"]
    27.5    and simple_function_diff[intro, simp] = simple_function_compose2[where h="(-)"]
    27.6    and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
    27.7 -  and simple_function_mult[intro, simp] = simple_function_compose2[where h="( * )"]
    27.8 +  and simple_function_mult[intro, simp] = simple_function_compose2[where h="(*)"]
    27.9    and simple_function_div[intro, simp] = simple_function_compose2[where h="(/)"]
   27.10    and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
   27.11    and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
   27.12 @@ -760,7 +760,7 @@
   27.13      using assms by (intro simple_function_partition) auto
   27.14    also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ennreal))`space M.
   27.15      if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"
   27.16 -    by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="( * )"] arg_cong2[where f=emeasure] sum.cong)
   27.17 +    by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="(*)"] arg_cong2[where f=emeasure] sum.cong)
   27.18    also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ennreal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))"
   27.19      using assms by (subst sum.If_cases) (auto intro!: simple_functionD(1) simp: eq)
   27.20    also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ennreal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"
    28.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Sep 23 21:49:31 2018 +0200
    28.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Mon Sep 24 14:30:09 2018 +0200
    28.3 @@ -1737,7 +1737,7 @@
    28.4    show ?thesis
    28.5      unfolding path_component_def 
    28.6    proof (intro exI conjI)
    28.7 -    have "continuous_on {0..1} (p \<circ> (( *) y))"
    28.8 +    have "continuous_on {0..1} (p \<circ> ((*) y))"
    28.9        apply (rule continuous_intros)+
   28.10        using p [unfolded path_def] y
   28.11        apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
    29.1 --- a/src/HOL/Analysis/Product_Vector.thy	Sun Sep 23 21:49:31 2018 +0200
    29.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Mon Sep 24 14:30:09 2018 +0200
    29.3 @@ -88,21 +88,21 @@
    29.4  
    29.5  end
    29.6  
    29.7 -lemma module_prod_scale_eq_scaleR: "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = scaleR"
    29.8 +lemma module_prod_scale_eq_scaleR: "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
    29.9    apply (rule ext) apply (rule ext)
   29.10    apply (subst module_prod.scale_def)
   29.11    subgoal by unfold_locales
   29.12    by (simp add: scaleR_prod_def)
   29.13  
   29.14  interpretation real_vector?: vector_space_prod "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
   29.15 -  rewrites "scale = (( *\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
   29.16 -    and "module.dependent ( *\<^sub>R) = dependent"
   29.17 -    and "module.representation ( *\<^sub>R) = representation"
   29.18 -    and "module.subspace ( *\<^sub>R) = subspace"
   29.19 -    and "module.span ( *\<^sub>R) = span"
   29.20 -    and "vector_space.extend_basis ( *\<^sub>R) = extend_basis"
   29.21 -    and "vector_space.dim ( *\<^sub>R) = dim"
   29.22 -    and "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
   29.23 +  rewrites "scale = ((*\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
   29.24 +    and "module.dependent (*\<^sub>R) = dependent"
   29.25 +    and "module.representation (*\<^sub>R) = representation"
   29.26 +    and "module.subspace (*\<^sub>R) = subspace"
   29.27 +    and "module.span (*\<^sub>R) = span"
   29.28 +    and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
   29.29 +    and "vector_space.dim (*\<^sub>R) = dim"
   29.30 +    and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
   29.31    subgoal by unfold_locales
   29.32    subgoal by (fact module_prod_scale_eq_scaleR)
   29.33    unfolding dependent_raw_def representation_raw_def subspace_raw_def span_raw_def
   29.34 @@ -539,11 +539,11 @@
   29.35  proof -
   29.36    interpret p1: Vector_Spaces.linear s1 scale "(\<lambda>x. (x, 0))"
   29.37      by unfold_locales (auto simp: scale_def)
   29.38 -  interpret pair1: finite_dimensional_vector_space_pair "( *a)" B1 scale Basis_pair
   29.39 +  interpret pair1: finite_dimensional_vector_space_pair "(*a)" B1 scale Basis_pair
   29.40      by unfold_locales
   29.41    interpret p2: Vector_Spaces.linear s2 scale "(\<lambda>x. (0, x))"
   29.42      by unfold_locales (auto simp: scale_def)
   29.43 -  interpret pair2: finite_dimensional_vector_space_pair "( *b)" B2 scale Basis_pair
   29.44 +  interpret pair2: finite_dimensional_vector_space_pair "(*b)" B2 scale Basis_pair
   29.45      by unfold_locales
   29.46    have ss: "p.subspace ((\<lambda>x. (x, 0)) ` S)" "p.subspace (Pair 0 ` T)"
   29.47      by (rule p1.subspace_image p2.subspace_image assms)+
    30.1 --- a/src/HOL/Analysis/Riemann_Mapping.thy	Sun Sep 23 21:49:31 2018 +0200
    30.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Sep 24 14:30:09 2018 +0200
    30.3 @@ -138,17 +138,17 @@
    30.4      proof (intro bdd_aboveI exI ballI, clarify)
    30.5        show "norm (deriv f 0) \<le> 1 / r" if "f \<in> F" for f
    30.6        proof -
    30.7 -        have r01: "( * ) (complex_of_real r) ` ball 0 1 \<subseteq> S"
    30.8 +        have r01: "(*) (complex_of_real r) ` ball 0 1 \<subseteq> S"
    30.9            using that \<open>r > 0\<close> by (auto simp: norm_mult r [THEN subsetD])
   30.10 -        then have "f holomorphic_on ( * ) (complex_of_real r) ` ball 0 1"
   30.11 +        then have "f holomorphic_on (*) (complex_of_real r) ` ball 0 1"
   30.12            using holomorphic_on_subset [OF holF] by (simp add: that)
   30.13          then have holf: "f \<circ> (\<lambda>z. (r * z)) holomorphic_on (ball 0 1)"
   30.14            by (intro holomorphic_intros holomorphic_on_compose)
   30.15 -        have f0: "(f \<circ> ( * ) (complex_of_real r)) 0 = 0"
   30.16 +        have f0: "(f \<circ> (*) (complex_of_real r)) 0 = 0"
   30.17            using F_def that by auto
   30.18          have "f ` S \<subseteq> ball 0 1"
   30.19            using F_def that by blast
   30.20 -        with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> ( * )(of_real r))z) < 1"
   30.21 +        with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> (*)(of_real r))z) < 1"
   30.22            by force
   30.23          have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
   30.24            if "z \<in> ball 0 1" for z::complex
   30.25 @@ -162,7 +162,7 @@
   30.26            using * [of 0] by simp
   30.27          have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
   30.28            using DERIV_imp_deriv df0 by blast
   30.29 -        have "norm (deriv (f \<circ> ( * ) (complex_of_real r)) 0) \<le> 1"
   30.30 +        have "norm (deriv (f \<circ> (*) (complex_of_real r)) 0) \<le> 1"
   30.31            by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
   30.32          with \<open>r > 0\<close> show ?thesis
   30.33            by (simp add: deq norm_mult divide_simps o_def)
    31.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Sep 23 21:49:31 2018 +0200
    31.2 +++ b/src/HOL/Analysis/Starlike.thy	Mon Sep 24 14:30:09 2018 +0200
    31.3 @@ -2902,22 +2902,22 @@
    31.4  lemma rel_interior_scaleR:
    31.5    fixes S :: "'n::euclidean_space set"
    31.6    assumes "c \<noteq> 0"
    31.7 -  shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
    31.8 -  using rel_interior_injective_linear_image[of "(( *\<^sub>R) c)" S]
    31.9 -    linear_conv_bounded_linear[of "( *\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
   31.10 +  shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
   31.11 +  using rel_interior_injective_linear_image[of "((*\<^sub>R) c)" S]
   31.12 +    linear_conv_bounded_linear[of "(*\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
   31.13    by auto
   31.14  
   31.15  lemma rel_interior_convex_scaleR:
   31.16    fixes S :: "'n::euclidean_space set"
   31.17    assumes "convex S"
   31.18 -  shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
   31.19 +  shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
   31.20    by (metis assms linear_scaleR rel_interior_convex_linear_image)
   31.21  
   31.22  lemma convex_rel_open_scaleR:
   31.23    fixes S :: "'n::euclidean_space set"
   31.24    assumes "convex S"
   31.25      and "rel_open S"
   31.26 -  shows "convex ((( *\<^sub>R) c) ` S) \<and> rel_open ((( *\<^sub>R) c) ` S)"
   31.27 +  shows "convex (((*\<^sub>R) c) ` S) \<and> rel_open (((*\<^sub>R) c) ` S)"
   31.28    by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
   31.29  
   31.30  lemma convex_rel_open_finite_inter:
   31.31 @@ -3086,10 +3086,10 @@
   31.32      by (simp add: rel_interior_empty cone_0)
   31.33  next
   31.34    case False
   31.35 -  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
   31.36 +  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
   31.37      using cone_iff[of S] assms by auto
   31.38    then have *: "0 \<in> ({0} \<union> rel_interior S)"
   31.39 -    and "\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
   31.40 +    and "\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
   31.41      by (auto simp add: rel_interior_scaleR)
   31.42    then show ?thesis
   31.43      using cone_iff[of "{0} \<union> rel_interior S"] by auto
   31.44 @@ -3099,7 +3099,7 @@
   31.45    fixes S :: "'m::euclidean_space set"
   31.46    assumes "convex S"
   31.47    shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow>
   31.48 -    c > 0 \<and> x \<in> ((( *\<^sub>R) c) ` (rel_interior S))"
   31.49 +    c > 0 \<and> x \<in> (((*\<^sub>R) c) ` (rel_interior S))"
   31.50  proof (cases "S = {}")
   31.51    case True
   31.52    then show ?thesis
   31.53 @@ -3132,9 +3132,9 @@
   31.54    {
   31.55      fix c :: real
   31.56      assume "c > 0"
   31.57 -    then have "f c = (( *\<^sub>R) c ` S)"
   31.58 +    then have "f c = ((*\<^sub>R) c ` S)"
   31.59        using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
   31.60 -    then have "rel_interior (f c) = ( *\<^sub>R) c ` rel_interior S"
   31.61 +    then have "rel_interior (f c) = (*\<^sub>R) c ` rel_interior S"
   31.62        using rel_interior_convex_scaleR[of S c] assms by auto
   31.63    }
   31.64    then show ?thesis using * ** by auto
   31.65 @@ -8025,7 +8025,7 @@
   31.66          by auto
   31.67        have "b \<bullet> (v - ?u) = 0" if "b \<in> B" for b
   31.68          using that \<open>finite B\<close>
   31.69 -        by (simp add: * algebra_simps inner_sum_right if_distrib [of "( *)v" for v] inner_commute cong: if_cong)
   31.70 +        by (simp add: * algebra_simps inner_sum_right if_distrib [of "(*)v" for v] inner_commute cong: if_cong)
   31.71        then show "y \<bullet> (v - ?u) = 0"
   31.72          by (simp add: u inner_sum_left)
   31.73      qed
    32.1 --- a/src/HOL/Analysis/normarith.ML	Sun Sep 23 21:49:31 2018 +0200
    32.2 +++ b/src/HOL/Analysis/normarith.ML	Mon Sep 24 14:30:09 2018 +0200
    32.3 @@ -26,7 +26,7 @@
    32.4   fun find_normedterms t acc = case Thm.term_of t of
    32.5      @{term "(+) :: real => _"}$_$_ =>
    32.6              find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
    32.7 -      | @{term "( * ) :: real => _"}$_$_ =>
    32.8 +      | @{term "(*) :: real => _"}$_$_ =>
    32.9              if not (is_ratconst (Thm.dest_arg1 t)) then acc else
   32.10              augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0)
   32.11                        (Thm.dest_arg t) acc
   32.12 @@ -83,7 +83,7 @@
   32.13  
   32.14  fun replacenegnorms cv t = case Thm.term_of t of
   32.15    @{term "(+) :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
   32.16 -| @{term "( * ) :: real => _"}$_$_ =>
   32.17 +| @{term "(*) :: real => _"}$_$_ =>
   32.18      if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
   32.19  | _ => Thm.reflexive t
   32.20  (*
    33.1 --- a/src/HOL/Binomial.thy	Sun Sep 23 21:49:31 2018 +0200
    33.2 +++ b/src/HOL/Binomial.thy	Mon Sep 24 14:30:09 2018 +0200
    33.3 @@ -1299,7 +1299,7 @@
    33.4    "n choose k =
    33.5        (if k > n then 0
    33.6         else if 2 * k > n then n choose (n - k)
    33.7 -       else (fold_atLeastAtMost_nat ( * ) (n - k + 1) n 1 div fact k))"
    33.8 +       else (fold_atLeastAtMost_nat (*) (n - k + 1) n 1 div fact k))"
    33.9  proof -
   33.10    {
   33.11      assume "k \<le> n"
    34.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Sep 23 21:49:31 2018 +0200
    34.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Mon Sep 24 14:30:09 2018 +0200
    34.3 @@ -421,7 +421,7 @@
    34.4      Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
    34.5      Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
    34.6      divide plus minus unit_factor normalize
    34.7 -    rewrites "dvd.dvd ( * ) = Rings.dvd"
    34.8 +    rewrites "dvd.dvd (*) = Rings.dvd"
    34.9      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   34.10    show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
   34.11    proof (rule ext)+
   34.12 @@ -575,7 +575,7 @@
   34.13      "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
   34.14      "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
   34.15      divide plus minus unit_factor normalize
   34.16 -    rewrites "dvd.dvd ( * ) = Rings.dvd"
   34.17 +    rewrites "dvd.dvd (*) = Rings.dvd"
   34.18      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   34.19    show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
   34.20    proof (rule ext)+
   34.21 @@ -612,7 +612,7 @@
   34.22      "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
   34.23      "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
   34.24      divide plus minus unit_factor normalize
   34.25 -    rewrites "dvd.dvd ( * ) = Rings.dvd"
   34.26 +    rewrites "dvd.dvd (*) = Rings.dvd"
   34.27      by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   34.28    show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
   34.29    proof (rule ext)+
    35.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Sep 23 21:49:31 2018 +0200
    35.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Sep 24 14:30:09 2018 +0200
    35.3 @@ -78,7 +78,7 @@
    35.4  
    35.5  instantiation fps :: ("{comm_monoid_add, times}") times
    35.6  begin
    35.7 -  definition fps_times_def: "( * ) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
    35.8 +  definition fps_times_def: "(*) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
    35.9    instance ..
   35.10  end
   35.11  
   35.12 @@ -2037,7 +2037,7 @@
   35.13    (* If f reprents {a_n} and P is a polynomial, then
   35.14          P(xD) f represents {P(n) a_n}*)
   35.15  
   35.16 -definition "fps_XD = ( * ) fps_X \<circ> fps_deriv"
   35.17 +definition "fps_XD = (*) fps_X \<circ> fps_deriv"
   35.18  
   35.19  lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)"
   35.20    by (simp add: fps_XD_def field_simps)
    36.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Sep 23 21:49:31 2018 +0200
    36.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 24 14:30:09 2018 +0200
    36.3 @@ -891,7 +891,7 @@
    36.4  lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
    36.5    by (induct n) (simp_all add: monom_0 monom_Suc)
    36.6  
    36.7 -lemma smult_Poly: "smult c (Poly xs) = Poly (map (( * ) c) xs)"
    36.8 +lemma smult_Poly: "smult c (Poly xs) = Poly (map ((*) c) xs)"
    36.9    by (auto simp: poly_eq_iff nth_default_def)
   36.10  
   36.11  lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)"
   36.12 @@ -3811,10 +3811,10 @@
   36.13    where
   36.14      "pseudo_divmod_main_list lc q r d (Suc n) =
   36.15        (let
   36.16 -        rr = map (( * ) lc) r;
   36.17 +        rr = map ((*) lc) r;
   36.18          a = hd r;
   36.19 -        qqq = cCons a (map (( * ) lc) q);
   36.20 -        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (( * ) a) d))
   36.21 +        qqq = cCons a (map ((*) lc) q);
   36.22 +        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d))
   36.23         in pseudo_divmod_main_list lc qqq rrr d n)"
   36.24    | "pseudo_divmod_main_list lc q r d 0 = (q, r)"
   36.25  
   36.26 @@ -3822,9 +3822,9 @@
   36.27    where
   36.28      "pseudo_mod_main_list lc r d (Suc n) =
   36.29        (let
   36.30 -        rr = map (( * ) lc) r;
   36.31 +        rr = map ((*) lc) r;
   36.32          a = hd r;
   36.33 -        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (( * ) a) d))
   36.34 +        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d))
   36.35         in pseudo_mod_main_list lc rrr d n)"
   36.36    | "pseudo_mod_main_list lc r d 0 = r"
   36.37  
   36.38 @@ -3836,7 +3836,7 @@
   36.39        (let
   36.40          a = hd r;
   36.41          qqq = cCons a q;
   36.42 -        rr = tl (if a = 0 then r else minus_poly_rev_list r (map (( * ) a) d))
   36.43 +        rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d))
   36.44         in divmod_poly_one_main_list qqq rr d n)"
   36.45    | "divmod_poly_one_main_list q r d 0 = (q, r)"
   36.46  
   36.47 @@ -3845,7 +3845,7 @@
   36.48      "mod_poly_one_main_list r d (Suc n) =
   36.49        (let
   36.50          a = hd r;
   36.51 -        rr = tl (if a = 0 then r else minus_poly_rev_list r (map (( * ) a) d))
   36.52 +        rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d))
   36.53         in mod_poly_one_main_list rr d n)"
   36.54    | "mod_poly_one_main_list r d 0 = r"
   36.55  
   36.56 @@ -3866,7 +3866,7 @@
   36.57          re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q)
   36.58         in rev re))"
   36.59  
   36.60 -lemma minus_zero_does_nothing: "minus_poly_rev_list x (map (( * ) 0) y) = x"
   36.61 +lemma minus_zero_does_nothing: "minus_poly_rev_list x (map ((*) 0) y) = x"
   36.62    for x :: "'a::ring list"
   36.63    by (induct x y rule: minus_poly_rev_list.induct) auto
   36.64  
   36.65 @@ -3874,8 +3874,8 @@
   36.66    by (induct xs ys rule: minus_poly_rev_list.induct) auto
   36.67  
   36.68  lemma if_0_minus_poly_rev_list:
   36.69 -  "(if a = 0 then x else minus_poly_rev_list x (map (( * ) a) y)) =
   36.70 -    minus_poly_rev_list x (map (( * ) a) y)"
   36.71 +  "(if a = 0 then x else minus_poly_rev_list x (map ((*) a) y)) =
   36.72 +    minus_poly_rev_list x (map ((*) a) y)"
   36.73    for a :: "'a::ring"
   36.74    by(cases "a = 0") (simp_all add: minus_zero_does_nothing)
   36.75  
   36.76 @@ -3917,7 +3917,7 @@
   36.77  
   36.78  lemma head_minus_poly_rev_list:
   36.79    "length d \<le> length r \<Longrightarrow> d \<noteq> [] \<Longrightarrow>
   36.80 -    hd (minus_poly_rev_list (map (( * ) (last d)) r) (map (( * ) (hd r)) (rev d))) = 0"
   36.81 +    hd (minus_poly_rev_list (map ((*) (last d)) r) (map ((*) (hd r)) (rev d))) = 0"
   36.82    for d r :: "'a::comm_ring list"
   36.83  proof (induct r)
   36.84    case Nil
   36.85 @@ -3927,7 +3927,7 @@
   36.86    then show ?case by (cases "rev d") (simp_all add: ac_simps)
   36.87  qed
   36.88  
   36.89 -lemma Poly_map: "Poly (map (( * ) a) p) = smult a (Poly p)"
   36.90 +lemma Poly_map: "Poly (map ((*) a) p) = smult a (Poly p)"
   36.91  proof (induct p)
   36.92    case Nil
   36.93    then show ?case by simp
   36.94 @@ -3955,9 +3955,9 @@
   36.95    with \<open>d \<noteq> []\<close> have "r \<noteq> []"
   36.96      using Suc_leI length_greater_0_conv list.size(3) by fastforce
   36.97    let ?a = "(hd (rev r))"
   36.98 -  let ?rr = "map (( * ) lc) (rev r)"
   36.99 -  let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map (( * ) ?a) (rev d))))"
  36.100 -  let ?qq = "cCons ?a (map (( * ) lc) q)"
  36.101 +  let ?rr = "map ((*) lc) (rev r)"
  36.102 +  let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map ((*) ?a) (rev d))))"
  36.103 +  let ?qq = "cCons ?a (map ((*) lc) q)"
  36.104    from * Suc(3) have n: "n = (1 + length r - length d - 1)"
  36.105      by simp
  36.106    from * have rr_val:"(length ?rrr) = (length r - 1)"
  36.107 @@ -3990,12 +3990,12 @@
  36.108      case 2
  36.109      show ?case
  36.110      proof (subst Poly_on_rev_starting_with_0, goal_cases)
  36.111 -      show "hd (minus_poly_rev_list (map (( * ) lc) (rev r)) (map (( * ) (hd (rev r))) (rev d))) = 0"
  36.112 +      show "hd (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))) = 0"
  36.113          by (fold lc, subst head_minus_poly_rev_list, insert * \<open>d \<noteq> []\<close>, auto)
  36.114        from * have "length d \<le> length r"
  36.115          by simp
  36.116        then show "smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d =
  36.117 -          Poly (rev (minus_poly_rev_list (map (( * ) lc) (rev r)) (map (( * ) (hd (rev r))) (rev d))))"
  36.118 +          Poly (rev (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))))"
  36.119          by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
  36.120              minus_poly_rev_list)
  36.121      qed
  36.122 @@ -4100,9 +4100,9 @@
  36.123          let
  36.124            cf = coeffs f;
  36.125            ilc = inverse (last cg);
  36.126 -          ch = map (( * ) ilc) cg;
  36.127 +          ch = map ((*) ilc) cg;
  36.128            (q, r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
  36.129 -        in (poly_of_list (map (( * ) ilc) q), poly_of_list (rev r)))"
  36.130 +        in (poly_of_list (map ((*) ilc) q), poly_of_list (rev r)))"
  36.131  proof -
  36.132    note d = pdivmod_via_pseudo_divmod pseudo_divmod_impl pseudo_divmod_list_def
  36.133    show ?thesis
  36.134 @@ -4121,10 +4121,10 @@
  36.135      have id2: "hd (rev (coeffs (smult ilc g))) = 1"
  36.136        by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def)
  36.137      have id3: "length (coeffs (smult ilc g)) = length (coeffs g)"
  36.138 -      "rev (coeffs (smult ilc g)) = rev (map (( * ) ilc) (coeffs g))"
  36.139 +      "rev (coeffs (smult ilc g)) = rev (map ((*) ilc) (coeffs g))"
  36.140        unfolding coeffs_smult using ilc by auto
  36.141      obtain q r where pair:
  36.142 -      "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (( * ) ilc) (coeffs g)))
  36.143 +      "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map ((*) ilc) (coeffs g)))
  36.144          (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
  36.145        by force
  36.146      show ?thesis
  36.147 @@ -4137,7 +4137,7 @@
  36.148  lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list"
  36.149  proof (intro ext, goal_cases)
  36.150    case (1 q r d n)
  36.151 -  have *: "map (( * ) 1) xs = xs" for xs :: "'a list"
  36.152 +  have *: "map ((*) 1) xs = xs" for xs :: "'a list"
  36.153      by (induct xs) auto
  36.154    show ?case
  36.155      by (induct n arbitrary: q r d) (auto simp: * Let_def)
  36.156 @@ -4151,7 +4151,7 @@
  36.157          in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let
  36.158          a = cr div lc;
  36.159          qq = cCons a q;
  36.160 -        rr = minus_poly_rev_list r (map (( * ) a) d)
  36.161 +        rr = minus_poly_rev_list r (map ((*) a) d)
  36.162         in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  36.163    | "divide_poly_main_list lc q r d 0 = q"
  36.164  
  36.165 @@ -4161,7 +4161,7 @@
  36.166        cr = hd r;
  36.167        a = cr div lc;
  36.168        qq = cCons a q;
  36.169 -      rr = minus_poly_rev_list r (map (( * ) a) d)
  36.170 +      rr = minus_poly_rev_list r (map ((*) a) d)
  36.171       in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
  36.172    by (simp add: Let_def minus_zero_does_nothing)
  36.173  
  36.174 @@ -4190,7 +4190,7 @@
  36.175          let
  36.176            cf = coeffs f;
  36.177            ilc = inverse (last cg);
  36.178 -          ch = map (( * ) ilc) cg;
  36.179 +          ch = map ((*) ilc) cg;
  36.180            r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
  36.181          in poly_of_list (rev r))"
  36.182    (is "_ = ?rhs")
  36.183 @@ -4209,9 +4209,9 @@
  36.184          let
  36.185            cf = coeffs f;
  36.186            ilc = inverse (last cg);
  36.187 -          ch = map (( * ) ilc) cg;
  36.188 +          ch = map ((*) ilc) cg;
  36.189            q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
  36.190 -        in poly_of_list ((map (( * ) ilc) q)))"
  36.191 +        in poly_of_list ((map ((*) ilc) q)))"
  36.192  
  36.193  text \<open>We do not declare the following lemma as code equation, since then polynomial division
  36.194    on non-fields will no longer be executable. However, a code-unfold is possible, since
  36.195 @@ -4259,7 +4259,7 @@
  36.196      with r d have id:
  36.197        "?thesis \<longleftrightarrow>
  36.198          Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
  36.199 -          (rev (rev (minus_poly_rev_list (rev rr) (rev (map (( * ) (lcr div lc)) dd))))) (rev d) n) =
  36.200 +          (rev (rev (minus_poly_rev_list (rev rr) (rev (map ((*) (lcr div lc)) dd))))) (rev d) n) =
  36.201            divide_poly_main lc
  36.202              (monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
  36.203              (Poly r - monom (lcr div lc) n * Poly d)
    37.1 --- a/src/HOL/Decision_Procs/Algebra_Aux.thy	Sun Sep 23 21:49:31 2018 +0200
    37.2 +++ b/src/HOL/Decision_Procs/Algebra_Aux.thy	Mon Sep 24 14:30:09 2018 +0200
    37.3 @@ -234,7 +234,7 @@
    37.4    by (induct n) (simp_all add: m_ac)
    37.5  
    37.6  definition cring_class_ops :: "'a::comm_ring_1 ring"
    37.7 -  where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
    37.8 +  where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
    37.9  
   37.10  lemma cring_class: "cring cring_class_ops"
   37.11    apply unfold_locales
    38.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sun Sep 23 21:49:31 2018 +0200
    38.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Sep 24 14:30:09 2018 +0200
    38.3 @@ -2402,7 +2402,7 @@
    38.4        @{code Add} (num_of_term vs t1, num_of_term vs t2)
    38.5    | num_of_term vs (@{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
    38.6        @{code Sub} (num_of_term vs t1, num_of_term vs t2)
    38.7 -  | num_of_term vs (@{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
    38.8 +  | num_of_term vs (@{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
    38.9        (case try HOLogic.dest_number t1 of
   38.10          SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
   38.11        | NONE =>
   38.12 @@ -2455,7 +2455,7 @@
   38.13        term_of_num vs t1 $ term_of_num vs t2
   38.14    | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} $
   38.15        term_of_num vs t1 $ term_of_num vs t2
   38.16 -  | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} $
   38.17 +  | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} $
   38.18        term_of_num vs (@{code C} i) $ term_of_num vs t2
   38.19    | term_of_num vs (@{code CN} (n, i, t)) =
   38.20        term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
    39.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Sep 23 21:49:31 2018 +0200
    39.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Sep 24 14:30:09 2018 +0200
    39.3 @@ -2476,7 +2476,7 @@
    39.4       @{code Add} (num_of_term vs t1, num_of_term vs t2)
    39.5    | num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
    39.6       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
    39.7 -  | num_of_term vs (@{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
    39.8 +  | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
    39.9       of @{code C} i => @{code Mul} (i, num_of_term vs t2)
   39.10        | _ => error "num_of_term: unsupported multiplication")
   39.11    | num_of_term vs (@{term "real_of_int :: int \<Rightarrow> real"} $ t') =
   39.12 @@ -2514,7 +2514,7 @@
   39.13        term_of_num vs t1 $ term_of_num vs t2
   39.14    | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $
   39.15        term_of_num vs t1 $ term_of_num vs t2
   39.16 -  | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $
   39.17 +  | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $
   39.18        term_of_num vs (@{code C} i) $ term_of_num vs t2
   39.19    | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
   39.20  
    40.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Sep 23 21:49:31 2018 +0200
    40.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Mon Sep 24 14:30:09 2018 +0200
    40.3 @@ -5579,7 +5579,7 @@
    40.4        @{code Add} (num_of_term vs t1, num_of_term vs t2)
    40.5    | num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
    40.6        @{code Sub} (num_of_term vs t1, num_of_term vs t2)
    40.7 -  | num_of_term vs (@{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
    40.8 +  | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
    40.9        (case (num_of_term vs t1)
   40.10         of @{code C} i => @{code Mul} (i, num_of_term vs t2)
   40.11          | _ => error "num_of_term: unsupported Multiplication")
   40.12 @@ -5638,7 +5638,7 @@
   40.13        term_of_num vs t1 $ term_of_num vs t2
   40.14    | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $
   40.15        term_of_num vs t1 $ term_of_num vs t2
   40.16 -  | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $
   40.17 +  | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $
   40.18        term_of_num vs (@{code C} i) $ term_of_num vs t2
   40.19    | term_of_num vs (@{code Floor} t) = @{term "of_int :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ term_of_num vs t)
   40.20    | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
    41.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Sep 23 21:49:31 2018 +0200
    41.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Sep 24 14:30:09 2018 +0200
    41.3 @@ -186,7 +186,7 @@
    41.4      by (cases "x = zero") (auto simp add: distrib_left ac_simps)
    41.5  qed
    41.6  
    41.7 -lemma (in comm_semiring_0) poly_cmult_map: "poly (map (( * ) c) p) x = c * poly p x"
    41.8 +lemma (in comm_semiring_0) poly_cmult_map: "poly (map ((*) c) p) x = c * poly p x"
    41.9    by (induct p) (auto simp add: distrib_left ac_simps)
   41.10  
   41.11  lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
    42.1 --- a/src/HOL/Deriv.thy	Sun Sep 23 21:49:31 2018 +0200
    42.2 +++ b/src/HOL/Deriv.thy	Mon Sep 24 14:30:09 2018 +0200
    42.3 @@ -38,7 +38,7 @@
    42.4  
    42.5  definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
    42.6      (infix "(has'_field'_derivative)" 50)
    42.7 -  where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative ( * ) D) F"
    42.8 +  where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative (*) D) F"
    42.9  
   42.10  lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
   42.11    by simp
   42.12 @@ -153,7 +153,7 @@
   42.13  
   42.14  lemma field_has_derivative_at:
   42.15    fixes x :: "'a::real_normed_field"
   42.16 -  shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
   42.17 +  shows "(f has_derivative (*) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
   42.18  proof -
   42.19    have "?lhs = (\<lambda>h. norm (f (x + h) - f x - D * h) / norm h) \<midarrow>0 \<rightarrow> 0"
   42.20      by (simp add: bounded_linear_mult_right has_derivative_at)
   42.21 @@ -648,7 +648,7 @@
   42.22    by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult.commute)
   42.23  
   42.24  lemma has_field_derivative_imp_has_derivative:
   42.25 -  "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative ( * ) D) F"
   42.26 +  "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative (*) D) F"
   42.27    by (simp add: has_field_derivative_def)
   42.28  
   42.29  lemma DERIV_subset:
   42.30 @@ -675,7 +675,7 @@
   42.31    assume "f differentiable at x within s"
   42.32    then obtain f' where *: "(f has_derivative f') (at x within s)"
   42.33      unfolding differentiable_def by auto
   42.34 -  then obtain c where "f' = (( * ) c)"
   42.35 +  then obtain c where "f' = ((*) c)"
   42.36      by (metis real_bounded_linear has_derivative_bounded_linear mult.commute fun_eq_iff)
   42.37    with * show "\<exists>D. (f has_real_derivative D) (at x within s)"
   42.38      unfolding has_field_derivative_def by auto
   42.39 @@ -702,7 +702,7 @@
   42.40  lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   42.41    unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
   42.42  
   42.43 -lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c"
   42.44 +lemma mult_commute_abs: "(\<lambda>x. x * c) = (*) c"
   42.45    for c :: "'a::ab_semigroup_mult"
   42.46    by (simp add: fun_eq_iff mult.commute)
   42.47  
   42.48 @@ -711,7 +711,7 @@
   42.49    assumes "DERIV f (g x) :> f'"
   42.50    assumes "(g has_derivative g') (at x within s)"
   42.51    shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
   42.52 -  using assms has_derivative_compose[of g g' x s f "( * ) f'"]
   42.53 +  using assms has_derivative_compose[of g g' x s f "(*) f'"]
   42.54    by (auto simp: has_field_derivative_def ac_simps)
   42.55  
   42.56  
   42.57 @@ -896,7 +896,7 @@
   42.58      ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
   42.59    using DERIV_cmult by (auto simp add: ac_simps)
   42.60  
   42.61 -lemma DERIV_cmult_Id [simp]: "(( * ) c has_field_derivative c) (at x within s)"
   42.62 +lemma DERIV_cmult_Id [simp]: "((*) c has_field_derivative c) (at x within s)"
   42.63    using DERIV_ident [THEN DERIV_cmult, where c = c and x = x] by simp
   42.64  
   42.65  lemma DERIV_cdivide:
   42.66 @@ -919,7 +919,7 @@
   42.67    shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x)))
   42.68      (at x within s)"
   42.69  proof -
   42.70 -  have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative ( * ) D)"
   42.71 +  have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative (*) D)"
   42.72      by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff)
   42.73    with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)"
   42.74      by (auto dest!: has_field_derivative_imp_has_derivative)
   42.75 @@ -972,7 +972,7 @@
   42.76  
   42.77  lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow>
   42.78    ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
   42.79 -  using has_derivative_compose[of f "( * ) D" x s g "( * ) E"]
   42.80 +  using has_derivative_compose[of f "(*) D" x s g "(*) E"]
   42.81    by (simp only: has_field_derivative_def mult_commute_abs ac_simps)
   42.82  
   42.83  corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
   42.84 @@ -990,7 +990,7 @@
   42.85    "(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow>
   42.86      (g has_field_derivative Db) (at x within s) \<Longrightarrow>
   42.87      (f \<circ> g has_field_derivative Da * Db) (at x within s)"
   42.88 -  using has_derivative_in_compose [of g "( * ) Db" x s f "( * ) Da "]
   42.89 +  using has_derivative_in_compose [of g "(*) Db" x s f "(*) Da "]
   42.90    by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps)
   42.91  
   42.92  (*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
    43.1 --- a/src/HOL/Enum.thy	Sun Sep 23 21:49:31 2018 +0200
    43.2 +++ b/src/HOL/Enum.thy	Mon Sep 24 14:30:09 2018 +0200
    43.3 @@ -585,7 +585,7 @@
    43.4  definition [simp]: "Groups.zero = a\<^sub>1"
    43.5  definition [simp]: "Groups.one = a\<^sub>1"
    43.6  definition [simp]: "(+) = (\<lambda>_ _. a\<^sub>1)"
    43.7 -definition [simp]: "( * ) = (\<lambda>_ _. a\<^sub>1)"
    43.8 +definition [simp]: "(*) = (\<lambda>_ _. a\<^sub>1)"
    43.9  definition [simp]: "(mod) = (\<lambda>_ _. a\<^sub>1)" 
   43.10  definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
   43.11  definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
   43.12 @@ -690,7 +690,7 @@
   43.13  definition "(-) = ((+) :: finite_2 \<Rightarrow> _)"
   43.14  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
   43.15  definition "inverse = (\<lambda>x :: finite_2. x)"
   43.16 -definition "divide = (( * ) :: finite_2 \<Rightarrow> _)"
   43.17 +definition "divide = ((*) :: finite_2 \<Rightarrow> _)"
   43.18  definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
   43.19  definition "abs = (\<lambda>x :: finite_2. x)"
   43.20  definition "sgn = (\<lambda>x :: finite_2. x)"
    44.1 --- a/src/HOL/Factorial.thy	Sun Sep 23 21:49:31 2018 +0200
    44.2 +++ b/src/HOL/Factorial.thy	Mon Sep 24 14:30:09 2018 +0200
    44.3 @@ -403,13 +403,13 @@
    44.4  subsection \<open>Misc\<close>
    44.5  
    44.6  lemma fact_code [code]:
    44.7 -  "fact n = (of_nat (fold_atLeastAtMost_nat (( * )) 2 n 1) :: 'a::semiring_char_0)"
    44.8 +  "fact n = (of_nat (fold_atLeastAtMost_nat ((*)) 2 n 1) :: 'a::semiring_char_0)"
    44.9  proof -
   44.10    have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
   44.11      by (simp add: fact_prod)
   44.12    also have "\<Prod>{1..n} = \<Prod>{2..n}"
   44.13      by (intro prod.mono_neutral_right) auto
   44.14 -  also have "\<dots> = fold_atLeastAtMost_nat (( * )) 2 n 1"
   44.15 +  also have "\<dots> = fold_atLeastAtMost_nat ((*)) 2 n 1"
   44.16      by (simp add: prod_atLeastAtMost_code)
   44.17    finally show ?thesis .
   44.18  qed
    45.1 --- a/src/HOL/GCD.thy	Sun Sep 23 21:49:31 2018 +0200
    45.2 +++ b/src/HOL/GCD.thy	Mon Sep 24 14:30:09 2018 +0200
    45.3 @@ -976,25 +976,25 @@
    45.4  lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
    45.5    by (blast dest: dvd_GcdD intro: Gcd_greatest)
    45.6  
    45.7 -lemma Gcd_mult: "Gcd (( *) c ` A) = normalize c * Gcd A"
    45.8 +lemma Gcd_mult: "Gcd ((*) c ` A) = normalize c * Gcd A"
    45.9  proof (cases "c = 0")
   45.10    case True
   45.11    then show ?thesis by auto
   45.12  next
   45.13    case [simp]: False
   45.14 -  have "Gcd (( *) c ` A) div c dvd Gcd A"
   45.15 +  have "Gcd ((*) c ` A) div c dvd Gcd A"
   45.16      by (intro Gcd_greatest, subst div_dvd_iff_mult)
   45.17         (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
   45.18 -  then have "Gcd (( *) c ` A) dvd c * Gcd A"
   45.19 +  then have "Gcd ((*) c ` A) dvd c * Gcd A"
   45.20      by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
   45.21    also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
   45.22      by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
   45.23 -  also have "Gcd (( *) c ` A) dvd \<dots> \<longleftrightarrow> Gcd (( *) c ` A) dvd normalize c * Gcd A"
   45.24 +  also have "Gcd ((*) c ` A) dvd \<dots> \<longleftrightarrow> Gcd ((*) c ` A) dvd normalize c * Gcd A"
   45.25      by (simp add: dvd_mult_unit_iff)
   45.26 -  finally have "Gcd (( *) c ` A) dvd normalize c * Gcd A" .
   45.27 -  moreover have "normalize c * Gcd A dvd Gcd (( *) c ` A)"
   45.28 +  finally have "Gcd ((*) c ` A) dvd normalize c * Gcd A" .
   45.29 +  moreover have "normalize c * Gcd A dvd Gcd ((*) c ` A)"
   45.30      by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
   45.31 -  ultimately have "normalize (Gcd (( *) c ` A)) = normalize (normalize c * Gcd A)"
   45.32 +  ultimately have "normalize (Gcd ((*) c ` A)) = normalize (normalize c * Gcd A)"
   45.33      by (rule associatedI)
   45.34    then show ?thesis
   45.35      by (simp add: normalize_mult)
   45.36 @@ -1015,10 +1015,10 @@
   45.37  
   45.38  lemma Lcm_mult:
   45.39    assumes "A \<noteq> {}"
   45.40 -  shows "Lcm (( *) c ` A) = normalize c * Lcm A"
   45.41 +  shows "Lcm ((*) c ` A) = normalize c * Lcm A"
   45.42  proof (cases "c = 0")
   45.43    case True
   45.44 -  with assms have "( *) c ` A = {0}"
   45.45 +  with assms have "(*) c ` A = {0}"
   45.46      by auto
   45.47    with True show ?thesis by auto
   45.48  next
   45.49 @@ -1027,23 +1027,23 @@
   45.50      by blast
   45.51    have "c dvd c * x"
   45.52      by simp
   45.53 -  also from x have "c * x dvd Lcm (( *) c ` A)"
   45.54 +  also from x have "c * x dvd Lcm ((*) c ` A)"
   45.55      by (intro dvd_Lcm) auto
   45.56 -  finally have dvd: "c dvd Lcm (( *) c ` A)" .
   45.57 -
   45.58 -  have "Lcm A dvd Lcm (( *) c ` A) div c"
   45.59 +  finally have dvd: "c dvd Lcm ((*) c ` A)" .
   45.60 +
   45.61 +  have "Lcm A dvd Lcm ((*) c ` A) div c"
   45.62      by (intro Lcm_least dvd_mult_imp_div)
   45.63        (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
   45.64 -  then have "c * Lcm A dvd Lcm (( *) c ` A)"
   45.65 +  then have "c * Lcm A dvd Lcm ((*) c ` A)"
   45.66      by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
   45.67    also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
   45.68      by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
   45.69 -  also have "\<dots> dvd Lcm (( *) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (( *) c ` A)"
   45.70 +  also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
   45.71      by (simp add: mult_unit_dvd_iff)
   45.72 -  finally have "normalize c * Lcm A dvd Lcm (( *) c ` A)" .
   45.73 -  moreover have "Lcm (( *) c ` A) dvd normalize c * Lcm A"
   45.74 +  finally have "normalize c * Lcm A dvd Lcm ((*) c ` A)" .
   45.75 +  moreover have "Lcm ((*) c ` A) dvd normalize c * Lcm A"
   45.76      by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
   45.77 -  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (( *) c ` A))"
   45.78 +  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm ((*) c ` A))"
   45.79      by (rule associatedI)
   45.80    then show ?thesis
   45.81      by (simp add: normalize_mult)
    46.1 --- a/src/HOL/Groups_List.thy	Sun Sep 23 21:49:31 2018 +0200
    46.2 +++ b/src/HOL/Groups_List.thy	Mon Sep 24 14:30:09 2018 +0200
    46.3 @@ -124,7 +124,7 @@
    46.4    by (induct xss) simp_all
    46.5  
    46.6  lemma (in monoid_add) length_product_lists:
    46.7 -  "length (product_lists xss) = foldr ( * ) (map length xss) 1"
    46.8 +  "length (product_lists xss) = foldr (*) (map length xss) 1"
    46.9  proof (induct xss)
   46.10    case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
   46.11  qed simp
    47.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Sep 23 21:49:31 2018 +0200
    47.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Sep 24 14:30:09 2018 +0200
    47.3 @@ -60,7 +60,7 @@
    47.4      and (OCaml) "Pervasives.( +. )"
    47.5  
    47.6  code_printing
    47.7 -  constant "( * ) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    47.8 +  constant "(*) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    47.9      (SML) "Real.* ((_), (_))"
   47.10      and (OCaml) "Pervasives.( *. )"
   47.11  
    48.1 --- a/src/HOL/Library/DAList_Multiset.thy	Sun Sep 23 21:49:31 2018 +0200
    48.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Mon Sep 24 14:30:09 2018 +0200
    48.3 @@ -372,7 +372,7 @@
    48.4  
    48.5  end
    48.6  
    48.7 -\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>( * )\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
    48.8 +\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>(*)\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
    48.9  lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((+) a) ^^ n)) 0 ms"
   48.10    unfolding sum_mset.eq_fold
   48.11    apply (rule comp_fun_commute.DAList_Multiset_fold)
   48.12 @@ -380,8 +380,8 @@
   48.13    apply (auto simp: ac_simps)
   48.14    done
   48.15  
   48.16 -\<comment> \<open>we cannot use \<open>\<lambda>a n. ( * ) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
   48.17 -lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((( * ) a) ^^ n)) 1 ms"
   48.18 +\<comment> \<open>we cannot use \<open>\<lambda>a n. (*) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
   48.19 +lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((*) a) ^^ n)) 1 ms"
   48.20    unfolding prod_mset.eq_fold
   48.21    apply (rule comp_fun_commute.DAList_Multiset_fold)
   48.22    apply unfold_locales
    49.1 --- a/src/HOL/Library/Discrete.thy	Sun Sep 23 21:49:31 2018 +0200
    49.2 +++ b/src/HOL/Library/Discrete.thy	Mon Sep 24 14:30:09 2018 +0200
    49.3 @@ -274,7 +274,7 @@
    49.4        then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
    49.5          using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
    49.6        then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
    49.7 -      moreover have "finite (( * ) q ` {m. m * m \<le> n})"
    49.8 +      moreover have "finite ((*) q ` {m. m * m \<le> n})"
    49.9          by (metis (mono_tags) finite_imageI finite_less_ub le_square)
   49.10        moreover have "\<exists>x. x * x \<le> n"
   49.11          by (metis \<open>q * q \<le> n\<close>)
   49.12 @@ -282,7 +282,7 @@
   49.13          by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
   49.14      qed
   49.15    qed
   49.16 -  then have "Max (( * ) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
   49.17 +  then have "Max ((*) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
   49.18      apply (subst Max_le_iff)
   49.19        apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
   49.20       apply auto
    50.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Sep 23 21:49:31 2018 +0200
    50.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Sep 24 14:30:09 2018 +0200
    50.3 @@ -262,7 +262,7 @@
    50.4  lift_definition one_ennreal :: ennreal is 1 by simp
    50.5  lift_definition zero_ennreal :: ennreal is 0 by simp
    50.6  lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(+)" by simp
    50.7 -lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "( * )" by simp
    50.8 +lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(*)" by simp
    50.9  
   50.10  instance
   50.11    by standard (transfer; auto simp: field_simps ereal_right_distrib)+
    51.1 --- a/src/HOL/Library/Float.thy	Sun Sep 23 21:49:31 2018 +0200
    51.2 +++ b/src/HOL/Library/Float.thy	Mon Sep 24 14:30:09 2018 +0200
    51.3 @@ -202,7 +202,7 @@
    51.4  lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(+)" by simp
    51.5  declare plus_float.rep_eq[simp]
    51.6  
    51.7 -lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "( * )" by simp
    51.8 +lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(*)" by simp
    51.9  declare times_float.rep_eq[simp]
   51.10  
   51.11  lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(-)" by simp
    52.1 --- a/src/HOL/Library/ListVector.thy	Sun Sep 23 21:49:31 2018 +0200
    52.2 +++ b/src/HOL/Library/ListVector.thy	Mon Sep 24 14:30:09 2018 +0200
    52.3 @@ -13,7 +13,7 @@
    52.4  text\<open>Multiplication with a scalar:\<close>
    52.5  
    52.6  abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
    52.7 -where "x *\<^sub>s xs \<equiv> map (( * ) x) xs"
    52.8 +where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
    52.9  
   52.10  lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
   52.11  by (induct xs) simp_all
    53.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Sep 23 21:49:31 2018 +0200
    53.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Sep 24 14:30:09 2018 +0200
    53.3 @@ -221,7 +221,7 @@
    53.4    val neg_tm = \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
    53.5    val add_tm = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
    53.6    val sub_tm = \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
    53.7 -  val mul_tm = \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close>
    53.8 +  val mul_tm = \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
    53.9    val inv_tm = \<^cterm>\<open>inverse :: real \<Rightarrow> _\<close>
   53.10    val div_tm = \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
   53.11    val pow_tm = \<^cterm>\<open>(^) :: real \<Rightarrow> _\<close>
   53.12 @@ -862,7 +862,7 @@
   53.13        Free (_, \<^typ>\<open>real\<close>) =>
   53.14          if not (member (op aconvc) fvs tm) then (@1, tm)
   53.15          else raise Failure "substitutable_monomial"
   53.16 -    | \<^term>\<open>( * ) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
   53.17 +    | \<^term>\<open>(*) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
   53.18          if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
   53.19            not (member (op aconvc) fvs (Thm.dest_arg tm))
   53.20          then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
   53.21 @@ -899,7 +899,7 @@
   53.22          val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
   53.23          val th1 =
   53.24            Drule.arg_cong_rule
   53.25 -            (Thm.apply \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
   53.26 +            (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
   53.27              (mk_meta_eq th)
   53.28          val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1
   53.29        in fconv_rule (arg_conv (real_poly_conv ctxt)) (isolate_variable v th2) end
   53.30 @@ -943,7 +943,7 @@
   53.31     \<^term>\<open>(=) :: real \<Rightarrow> _\<close>, \<^term>\<open>(<) :: real \<Rightarrow> _\<close>,
   53.32     \<^term>\<open>(\<le>) :: real \<Rightarrow> _\<close>,
   53.33     \<^term>\<open>(+) :: real \<Rightarrow> _\<close>, \<^term>\<open>(-) :: real \<Rightarrow> _\<close>,
   53.34 -   \<^term>\<open>( * ) :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
   53.35 +   \<^term>\<open>(*) :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
   53.36     \<^term>\<open>(/) :: real \<Rightarrow> _\<close>, \<^term>\<open>inverse :: real \<Rightarrow> _\<close>,
   53.37     \<^term>\<open>(^) :: real \<Rightarrow> _\<close>, \<^term>\<open>abs :: real \<Rightarrow> _\<close>,
   53.38     \<^term>\<open>min :: real \<Rightarrow> _\<close>, \<^term>\<open>max :: real \<Rightarrow> _\<close>,
    54.1 --- a/src/HOL/Library/positivstellensatz.ML	Sun Sep 23 21:49:31 2018 +0200
    54.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Sep 24 14:30:09 2018 +0200
    54.3 @@ -328,13 +328,13 @@
    54.4      let
    54.5        val m' = FuncUtil.dest_monomial m
    54.6        val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
    54.7 -    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close> s) t) vps
    54.8 +    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> s) t) vps
    54.9      end
   54.10  
   54.11  fun cterm_of_cmonomial (m,c) =
   54.12    if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   54.13    else if c = @1 then cterm_of_monomial m
   54.14 -  else Thm.apply (Thm.apply \<^cterm>\<open>( * )::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
   54.15 +  else Thm.apply (Thm.apply \<^cterm>\<open>(*)::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
   54.16  
   54.17  fun cterm_of_poly p =
   54.18    if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\<open>0::real\<close>
   54.19 @@ -680,7 +680,7 @@
   54.20            in
   54.21              if opr aconvc \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
   54.22              then linear_add (lin_of_hol l) (lin_of_hol r)
   54.23 -            else if opr aconvc \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close>
   54.24 +            else if opr aconvc \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
   54.25                      andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   54.26              else FuncUtil.Ctermfunc.onefunc (ct, @1)
   54.27            end
    55.1 --- a/src/HOL/Limits.thy	Sun Sep 23 21:49:31 2018 +0200
    55.2 +++ b/src/HOL/Limits.thy	Mon Sep 24 14:30:09 2018 +0200
    55.3 @@ -826,7 +826,7 @@
    55.4  
    55.5  lemma continuous_on_mult_const [simp]:
    55.6    fixes c::"'a::real_normed_algebra"
    55.7 -  shows "continuous_on s (( *) c)"
    55.8 +  shows "continuous_on s ((*) c)"
    55.9    by (intro continuous_on_mult_left continuous_on_id)
   55.10  
   55.11  lemma tendsto_divide_zero:
    56.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Sun Sep 23 21:49:31 2018 +0200
    56.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Mon Sep 24 14:30:09 2018 +0200
    56.3 @@ -1487,7 +1487,7 @@
    56.4  begin
    56.5  
    56.6  definition
    56.7 -  times_matrix_def: "A * B = mult_matrix (( * )) (+) A B"
    56.8 +  times_matrix_def: "A * B = mult_matrix ((*)) (+) A B"
    56.9  
   56.10  instance ..
   56.11  
   56.12 @@ -1795,7 +1795,7 @@
   56.13  by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
   56.14  
   56.15  definition scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" where
   56.16 -  "scalar_mult a m == apply_matrix (( * ) a) m"
   56.17 +  "scalar_mult a m == apply_matrix ((*) a) m"
   56.18  
   56.19  lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
   56.20  by (simp add: scalar_mult_def)
    57.1 --- a/src/HOL/Modules.thy	Sun Sep 23 21:49:31 2018 +0200
    57.2 +++ b/src/HOL/Modules.thy	Mon Sep 24 14:30:09 2018 +0200
    57.3 @@ -878,9 +878,9 @@
    57.4  
    57.5  lemma module_hom_compose_scale:
    57.6    "module_hom s1 s2 (\<lambda>x. s2 (f x) (c))"
    57.7 -  if "module_hom s1 ( *) f"
    57.8 +  if "module_hom s1 (*) f"
    57.9  proof -
   57.10 -  interpret mh: module_hom s1 "( *)" f by fact
   57.11 +  interpret mh: module_hom s1 "(*)" f by fact
   57.12    show ?thesis
   57.13      by unfold_locales (simp_all add: mh.add mh.scale m2.scale_left_distrib)
   57.14  qed
   57.15 @@ -913,7 +913,7 @@
   57.16    using module_axioms module_hom_iff scale_left_commute scale_right_distrib by blast
   57.17  
   57.18  lemma module_hom_scale_left[simp]:
   57.19 -  "module_hom ( *) scale (\<lambda>r. scale r x)"
   57.20 +  "module_hom (*) scale (\<lambda>r. scale r x)"
   57.21    by unfold_locales (auto simp: algebra_simps)
   57.22  
   57.23  lemma module_hom_id: "module_hom scale scale id"
    58.1 --- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Sep 23 21:49:31 2018 +0200
    58.2 +++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Sep 24 14:30:09 2018 +0200
    58.3 @@ -223,7 +223,7 @@
    58.4  lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1"
    58.5    by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
    58.6  
    58.7 -lemma NSDERIV_cmult_Id [simp]: "NSDERIV (( * ) c) x :> c"
    58.8 +lemma NSDERIV_cmult_Id [simp]: "NSDERIV ((*) c) x :> c"
    58.9    using NSDERIV_Id [THEN NSDERIV_cmult] by simp
   58.10  
   58.11  lemma NSDERIV_inverse:
    59.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Sep 23 21:49:31 2018 +0200
    59.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Sep 24 14:30:09 2018 +0200
    59.3 @@ -413,7 +413,7 @@
    59.4  
    59.5  instantiation star :: (times) times
    59.6  begin
    59.7 -  definition star_mult_def: "(( * )) \<equiv> *f2* (( * ))"
    59.8 +  definition star_mult_def: "((*)) \<equiv> *f2* ((*))"
    59.9    instance ..
   59.10  end
   59.11  
    60.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sun Sep 23 21:49:31 2018 +0200
    60.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Sep 24 14:30:09 2018 +0200
    60.3 @@ -731,7 +731,7 @@
    60.4  
    60.5  (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
    60.6  
    60.7 -definition "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
    60.8 +definition "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
    60.9  
   60.10  lemma primefact:
   60.11    fixes n :: nat
   60.12 @@ -743,8 +743,8 @@
   60.13    from assms have "n = prod_mset (prime_factorization n)"
   60.14      by (simp add: prod_mset_prime_factorization)
   60.15    also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
   60.16 -  also have "\<dots> = foldr ( * ) xs 1" by (induct xs) simp_all
   60.17 -  finally have "foldr ( * ) xs 1 = n" ..
   60.18 +  also have "\<dots> = foldr (*) xs 1" by (induct xs) simp_all
   60.19 +  finally have "foldr (*) xs 1 = n" ..
   60.20    moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto
   60.21    ultimately have "primefact xs n" by (auto simp: primefact_def)
   60.22    then show ?thesis ..
   60.23 @@ -763,10 +763,10 @@
   60.24  next
   60.25    case (Cons q qs)
   60.26    from Cons.prems[unfolded primefact_def]
   60.27 -  have q: "prime q" "q * foldr ( * ) qs 1 = n" "\<forall>p \<in>set qs. prime p"
   60.28 -    and p: "prime p" "p dvd q * foldr ( * ) qs 1"
   60.29 +  have q: "prime q" "q * foldr (*) qs 1 = n" "\<forall>p \<in>set qs. prime p"
   60.30 +    and p: "prime p" "p dvd q * foldr (*) qs 1"
   60.31      by simp_all
   60.32 -  consider "p dvd q" | "p dvd foldr ( * ) qs 1"
   60.33 +  consider "p dvd q" | "p dvd foldr (*) qs 1"
   60.34      by (metis p prime_dvd_mult_eq_nat)
   60.35    then show ?case
   60.36    proof cases
   60.37 @@ -776,19 +776,19 @@
   60.38      then show ?thesis by simp
   60.39    next
   60.40      case prem: 2
   60.41 -    from q(3) have pqs: "primefact qs (foldr ( * ) qs 1)"
   60.42 +    from q(3) have pqs: "primefact qs (foldr (*) qs 1)"
   60.43        by (simp add: primefact_def)
   60.44      from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp
   60.45    qed
   60.46  qed
   60.47  
   60.48 -lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> list_all prime ps"
   60.49 +lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> list_all prime ps"
   60.50    by (auto simp add: primefact_def list_all_iff)
   60.51  
   60.52  text \<open>Variant of Lucas theorem.\<close>
   60.53  lemma lucas_primefact:
   60.54    assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
   60.55 -    and psn: "foldr ( * ) ps 1 = n - 1"
   60.56 +    and psn: "foldr (*) ps 1 = n - 1"
   60.57      and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
   60.58    shows "prime n"
   60.59  proof -
   60.60 @@ -806,7 +806,7 @@
   60.61  text \<open>Variant of Pocklington theorem.\<close>
   60.62  lemma pocklington_primefact:
   60.63    assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
   60.64 -    and arnb: "(a^r) mod n = b" and psq: "foldr ( * ) ps 1 = q"
   60.65 +    and arnb: "(a^r) mod n = b" and psq: "foldr (*) ps 1 = q"
   60.66      and bqn: "(b^q) mod n = 1"
   60.67      and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
   60.68    shows "prime n"
    61.1 --- a/src/HOL/Number_Theory/Totient.thy	Sun Sep 23 21:49:31 2018 +0200
    61.2 +++ b/src/HOL/Number_Theory/Totient.thy	Mon Sep 24 14:30:09 2018 +0200
    61.3 @@ -239,11 +239,11 @@
    61.4    assumes "prime p"
    61.5    shows   "totient (p ^ Suc n) = p ^ n * (p - 1)"
    61.6  proof -
    61.7 -  from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - ( * ) p ` {0<..p ^ n})"
    61.8 +  from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - (*) p ` {0<..p ^ n})"
    61.9      unfolding totient_def by (subst totatives_prime_power_Suc) simp_all
   61.10 -  also from assms have "\<dots> = p ^ Suc n - card (( * ) p ` {0<..p^n})"
   61.11 +  also from assms have "\<dots> = p ^ Suc n - card ((*) p ` {0<..p^n})"
   61.12      by (subst card_Diff_subset) (auto intro: prime_gt_0_nat)
   61.13 -  also from assms have "card (( * ) p ` {0<..p^n}) = p ^ n"
   61.14 +  also from assms have "card ((*) p ` {0<..p^n}) = p ^ n"
   61.15      by (subst card_image) (auto simp: inj_on_def)
   61.16    also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps)
   61.17    finally show ?thesis .
    62.1 --- a/src/HOL/Probability/Independent_Family.thy	Sun Sep 23 21:49:31 2018 +0200
    62.2 +++ b/src/HOL/Probability/Independent_Family.thy	Mon Sep 24 14:30:09 2018 +0200
    62.3 @@ -1165,7 +1165,7 @@
    62.4    also have "...=  prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
    62.5      by (auto intro!: indep_varD[where Ma=N and Mb=N])
    62.6    also have "... = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
    62.7 -    by (auto intro!: arg_cong2[where f= "( * )"] arg_cong[where f= prob])
    62.8 +    by (auto intro!: arg_cong2[where f= "(*)"] arg_cong[where f= prob])
    62.9    finally show ?thesis .
   62.10  qed
   62.11  
    63.1 --- a/src/HOL/Probability/PMF_Impl.thy	Sun Sep 23 21:49:31 2018 +0200
    63.2 +++ b/src/HOL/Probability/PMF_Impl.thy	Mon Sep 24 14:30:09 2018 +0200
    63.3 @@ -231,7 +231,7 @@
    63.4  qualified lemma mapping_of_bind_pmf:
    63.5    assumes "finite (set_pmf p)"
    63.6    shows   "mapping_of_pmf (bind_pmf p f) = 
    63.7 -             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x)) 
    63.8 +             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x)) 
    63.9                 (mapping_of_pmf (f x))) (set_pmf p)"
   63.10    using assms
   63.11    by (intro mapping_of_pmfI')
   63.12 @@ -268,7 +268,7 @@
   63.13  lemma bind_pmf_aux_code_aux:
   63.14    assumes "finite A"
   63.15    shows   "bind_pmf_aux p f A = 
   63.16 -             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
   63.17 +             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
   63.18                 (mapping_of_pmf (f x))) A" (is "?lhs = ?rhs")
   63.19  proof (intro mapping_eqI'[where d = 0])
   63.20    fix x assume "x \<in> Mapping.keys ?lhs"
   63.21 @@ -287,7 +287,7 @@
   63.22  
   63.23  lemma bind_pmf_aux_code [code]:
   63.24    "bind_pmf_aux p f (set xs) = 
   63.25 -     fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
   63.26 +     fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
   63.27                 (mapping_of_pmf (f x))) (set xs)"
   63.28    by (rule bind_pmf_aux_code_aux) simp_all
   63.29  
    64.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Sep 23 21:49:31 2018 +0200
    64.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Sep 24 14:30:09 2018 +0200
    64.3 @@ -78,7 +78,7 @@
    64.4  done
    64.5  
    64.6  quotient_definition
    64.7 -  "(( * )) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
    64.8 +  "((*)) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
    64.9    apply(rule equivp_transp[OF int_equivp])
   64.10    apply(rule times_int_raw_fst)
   64.11    apply(assumption)
    65.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Sep 23 21:49:31 2018 +0200
    65.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Mon Sep 24 14:30:09 2018 +0200
    65.3 @@ -41,7 +41,7 @@
    65.4    "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
    65.5  
    65.6  quotient_definition
    65.7 -  "(( * )) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute)
    65.8 +  "((*)) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute)
    65.9  
   65.10  fun plus_rat_raw where
   65.11    "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
    66.1 --- a/src/HOL/Real.thy	Sun Sep 23 21:49:31 2018 +0200
    66.2 +++ b/src/HOL/Real.thy	Mon Sep 24 14:30:09 2018 +0200
    66.3 @@ -32,7 +32,7 @@
    66.4    for x :: "'a::cancel_semigroup_add"
    66.5    by (meson add_left_imp_eq injI)
    66.6  
    66.7 -lemma inj_mult_left [simp]: "inj (( * ) x) \<longleftrightarrow> x \<noteq> 0"
    66.8 +lemma inj_mult_left [simp]: "inj ((*) x) \<longleftrightarrow> x \<noteq> 0"
    66.9    for x :: "'a::idom"
   66.10    by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
   66.11  
    67.1 --- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Sun Sep 23 21:49:31 2018 +0200
    67.2 +++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Mon Sep 24 14:30:09 2018 +0200
    67.3 @@ -603,7 +603,7 @@
    67.4      hence "(\<lambda>n. (-(x^2))^n) sums (1 / (1 - (-(x^2))))" by (intro geometric_sums) simp_all
    67.5      also have "1 - (-(x^2)) = 1 + x^2" by simp
    67.6      also have "(\<lambda>n. (-(x^2))^n) = (\<lambda>n. ?f (2*n))" by (auto simp: fun_eq_iff power_minus' power_mult)
    67.7 -    also have "range (( *) (2::nat)) = {n. even n}"
    67.8 +    also have "range ((*) (2::nat)) = {n. even n}"
    67.9        by (auto elim!: evenE)
   67.10      hence "(\<lambda>n. ?f (2*n)) sums (1 / (1 + x^2)) \<longleftrightarrow> ?f sums (1 / (1 + x^2))"
   67.11        by (intro sums_mono_reindex) (simp_all add: strict_mono_Suc_iff)
   67.12 @@ -1225,11 +1225,11 @@
   67.13        | (xs, MSLNil) \<Rightarrow> MSLNil
   67.14        | (MSLCons x xs, MSLCons y ys) \<Rightarrow>
   67.15             MSLCons (fst x * fst y, snd x + snd y) 
   67.16 -             (plus_ms_aux (mslmap (map_prod (( *) (fst x)) ((+) (snd x))) ys)
   67.17 +             (plus_ms_aux (mslmap (map_prod ((*) (fst x)) ((+) (snd x))) ys)
   67.18                 (times_ms_aux xs (MSLCons y ys))))"
   67.19  
   67.20  definition scale_shift_ms_aux :: "('a :: times \<times> real) \<Rightarrow> ('a \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
   67.21 -  "scale_shift_ms_aux = (\<lambda>(a,b) xs. mslmap (map_prod (( *) a) ((+) b)) xs)"
   67.22 +  "scale_shift_ms_aux = (\<lambda>(a,b) xs. mslmap (map_prod ((*) a) ((+) b)) xs)"
   67.23  
   67.24  lemma times_ms_aux_altdef:
   67.25    "times_ms_aux xs ys = 
   67.26 @@ -1282,7 +1282,7 @@
   67.27  qed
   67.28  
   67.29  lemma scale_shift_ms_aux_conv_mslmap: 
   67.30 -  "scale_shift_ms_aux x = mslmap (map_prod (( *) (fst x)) ((+) (snd x)))"
   67.31 +  "scale_shift_ms_aux x = mslmap (map_prod ((*) (fst x)) ((+) (snd x)))"
   67.32    by (rule ext) (simp add: scale_shift_ms_aux_def map_prod_def case_prod_unfold)
   67.33  
   67.34  fun inverse_ms_aux :: "('a :: multiseries \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
   67.35 @@ -2525,7 +2525,7 @@
   67.36    have "times_ms_aux (MSLCons (const_expansion 1, 0) MSLNil) xs = xs" for xs :: "('a \<times> real) msllist"
   67.37    proof (coinduction arbitrary: xs rule: msllist.coinduct_upto)
   67.38      case Eq_real_prod_msllist
   67.39 -    have "map_prod (( *) (const_expansion 1 :: 'a)) ((+) (0::real)) = (\<lambda>x. x)"
   67.40 +    have "map_prod ((*) (const_expansion 1 :: 'a)) ((+) (0::real)) = (\<lambda>x. x)"
   67.41        by (rule ext) (simp add: map_prod_def times_const_expansion_1 case_prod_unfold)
   67.42      moreover have "mslmap \<dots> = (\<lambda>x. x)" by (rule ext) (simp add: msllist.map_ident)
   67.43      ultimately have "scale_shift_ms_aux (const_expansion 1 :: 'a, 0) = (\<lambda>x. x)"
    68.1 --- a/src/HOL/Real_Asymp/Real_Asymp_Approx.thy	Sun Sep 23 21:49:31 2018 +0200
    68.2 +++ b/src/HOL/Real_Asymp/Real_Asymp_Approx.thy	Mon Sep 24 14:30:09 2018 +0200
    68.3 @@ -39,7 +39,7 @@
    68.4  
    68.5  fun eval_nat (@{term "(+) :: nat => _"} $ a $ b) = bin (op +) (a, b)
    68.6    | eval_nat (@{term "(-) :: nat => _"} $ a $ b) = bin (clamp o op -) (a, b)
    68.7 -  | eval_nat (@{term "( * ) :: nat => _"} $ a $ b) = bin (op *) (a, b)
    68.8 +  | eval_nat (@{term "(*) :: nat => _"} $ a $ b) = bin (op *) (a, b)
    68.9    | eval_nat (@{term "(div) :: nat => _"} $ a $ b) = bin Int.div (a, b)
   68.10    | eval_nat (@{term "(^) :: nat => _"} $ a $ b) = bin (fn (a,b) => Integer.pow a b) (a, b)
   68.11    | eval_nat (t as (@{term "numeral :: _ => nat"} $ _)) = snd (HOLogic.dest_number t)
   68.12 @@ -65,7 +65,7 @@
   68.13  
   68.14  fun eval (@{term "(+) :: real => _"} $ a $ b) = eval a + eval b
   68.15    | eval (@{term "(-) :: real => _"} $ a $ b) = eval a - eval b
   68.16 -  | eval (@{term "( * ) :: real => _"} $ a $ b) = eval a * eval b
   68.17 +  | eval (@{term "(*) :: real => _"} $ a $ b) = eval a * eval b
   68.18    | eval (@{term "(/) :: real => _"} $ a $ b) =
   68.19        let val a = eval a; val b = eval b in
   68.20          if Real.==(b, Real.fromInt 0) then nan else a / b
    69.1 --- a/src/HOL/Real_Asymp/exp_log_expression.ML	Sun Sep 23 21:49:31 2018 +0200
    69.2 +++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Mon Sep 24 14:30:09 2018 +0200
    69.3 @@ -257,7 +257,7 @@
    69.4        | expr_to_term' (Add (a, b)) = 
    69.5            @{term "(+) :: real => _"} $ expr_to_term' a $ expr_to_term' b
    69.6        | expr_to_term' (Mult (a, b)) = 
    69.7 -          @{term "( *) :: real => _"} $ expr_to_term' a $ expr_to_term' b
    69.8 +          @{term "(*) :: real => _"} $ expr_to_term' a $ expr_to_term' b
    69.9        | expr_to_term' (Minus (a, b)) = 
   69.10            @{term "(-) :: real => _"} $ expr_to_term' a $ expr_to_term' b
   69.11        | expr_to_term' (Div (a, b)) = 
   69.12 @@ -354,7 +354,7 @@
   69.13            Add (reify' s, reify' t)
   69.14        | reify'' (@{term "(-) :: real => _"} $ s $ t) =
   69.15            Minus (reify' s, reify' t)
   69.16 -      | reify'' (@{term "( *) :: real => _"} $ s $ t) =
   69.17 +      | reify'' (@{term "(*) :: real => _"} $ s $ t) =
   69.18            Mult (reify' s, reify' t)
   69.19        | reify'' (@{term "(/) :: real => _"} $ s $ t) =
   69.20            Div (reify' s, reify' t)
   69.21 @@ -435,7 +435,7 @@
   69.22            Add (reify'' s, reify'' t)
   69.23        | reify'' (@{term "(-) :: real => _"} $ s $ t) =
   69.24            Minus (reify'' s, reify'' t)
   69.25 -      | reify'' (@{term "( *) :: real => _"} $ s $ t) =
   69.26 +      | reify'' (@{term "(*) :: real => _"} $ s $ t) =
   69.27            Mult (reify'' s, reify'' t)
   69.28        | reify'' (@{term "(/) :: real => _"} $ s $ t) =
   69.29            Div (reify'' s, reify'' t)
   69.30 @@ -509,7 +509,7 @@
   69.31        "(" ^ simple_print_const a ^ "+" ^ simple_print_const b ^ ")"
   69.32    | simple_print_const (@{term "(-) :: real => _"} $ a $ b) =
   69.33        "(" ^ simple_print_const a ^ "-" ^ simple_print_const b ^ ")"
   69.34 -  | simple_print_const (@{term "( * ) :: real => _"} $ a $ b) =
   69.35 +  | simple_print_const (@{term "(*) :: real => _"} $ a $ b) =
   69.36        "(" ^ simple_print_const a ^ "*" ^ simple_print_const b ^ ")"
   69.37    | simple_print_const (@{term "inverse :: real => _"} $ a) =
   69.38        "(1 / " ^ simple_print_const a ^ ")"
    70.1 --- a/src/HOL/Real_Asymp/multiseries_expansion.ML	Sun Sep 23 21:49:31 2018 +0200
    70.2 +++ b/src/HOL/Real_Asymp/multiseries_expansion.ML	Mon Sep 24 14:30:09 2018 +0200
    70.3 @@ -2262,7 +2262,7 @@
    70.4        else if b aconv @{term "\<lambda>_::real. -1 :: real"} then
    70.5          Term.betapply (@{term "\<lambda>(f::real\<Rightarrow>real) x. -f x"}, a)
    70.6        else
    70.7 -        Abs ("x", @{typ real}, @{term "( *) :: real => _"} $
    70.8 +        Abs ("x", @{typ real}, @{term "(*) :: real => _"} $
    70.9            (Term.betapply (a, Bound 0)) $ (Term.betapply (b, Bound 0)))
   70.10  
   70.11      fun mk_powr b e =
    71.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Sep 23 21:49:31 2018 +0200
    71.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Sep 24 14:30:09 2018 +0200
    71.3 @@ -53,8 +53,8 @@
    71.4  end
    71.5  
    71.6  global_interpretation real_vector?: vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
    71.7 -  rewrites "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
    71.8 -    and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
    71.9 +  rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
   71.10 +    and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
   71.11    defines dependent_raw_def: dependent = real_vector.dependent
   71.12      and representation_raw_def: representation = real_vector.representation
   71.13      and subspace_raw_def: subspace = real_vector.subspace
   71.14 @@ -82,8 +82,8 @@
   71.15  abbreviation "independent x \<equiv> \<not> dependent x"
   71.16  
   71.17  global_interpretation real_vector?: vector_space_pair "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
   71.18 -  rewrites  "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
   71.19 -    and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
   71.20 +  rewrites  "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
   71.21 +    and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
   71.22    defines construct_raw_def: construct = real_vector.construct
   71.23    apply unfold_locales
   71.24    unfolding linear_def real_scaleR_def
   71.25 @@ -1316,7 +1316,7 @@
   71.26  
   71.27  corollary real_linearD:
   71.28    fixes f :: "real \<Rightarrow> real"
   71.29 -  assumes "linear f" obtains c where "f = ( *) c"
   71.30 +  assumes "linear f" obtains c where "f = (*) c"
   71.31    by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
   71.32  
   71.33  lemma linear_times_of_real: "linear (\<lambda>x. a * of_real x)"
   71.34 @@ -1439,7 +1439,7 @@
   71.35  
   71.36  lemma comp1:
   71.37    assumes "bounded_linear g"
   71.38 -  shows "bounded_bilinear (\<lambda>x. ( **) (g x))"
   71.39 +  shows "bounded_bilinear (\<lambda>x. (**) (g x))"
   71.40  proof unfold_locales
   71.41    interpret g: bounded_linear g by fact
   71.42    show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
   71.43 @@ -1537,7 +1537,7 @@
   71.44    qed
   71.45  qed
   71.46  
   71.47 -lemma bounded_bilinear_mult: "bounded_bilinear (( *) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
   71.48 +lemma bounded_bilinear_mult: "bounded_bilinear ((*) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
   71.49    apply (rule bounded_bilinear.intro)
   71.50        apply (auto simp: algebra_simps)
   71.51    apply (rule_tac x=1 in exI)
    72.1 --- a/src/HOL/SMT.thy	Sun Sep 23 21:49:31 2018 +0200
    72.2 +++ b/src/HOL/SMT.thy	Mon Sep 24 14:30:09 2018 +0200
    72.3 @@ -134,7 +134,7 @@
    72.4  lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
    72.5  lemma nat_plus_as_int: "(+) = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
    72.6  lemma nat_minus_as_int: "(-) = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
    72.7 -lemma nat_times_as_int: "( * ) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
    72.8 +lemma nat_times_as_int: "(*) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
    72.9  lemma nat_div_as_int: "(div) = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
   72.10  lemma nat_mod_as_int: "(mod) = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
   72.11  
    73.1 --- a/src/HOL/Set_Interval.thy	Sun Sep 23 21:49:31 2018 +0200
    73.2 +++ b/src/HOL/Set_Interval.thy	Mon Sep 24 14:30:09 2018 +0200
    73.3 @@ -1015,12 +1015,12 @@
    73.4  context linordered_field begin
    73.5  
    73.6  lemma image_mult_atLeastAtMost [simp]:
    73.7 -  "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
    73.8 +  "((*) d ` {a..b}) = {d*a..d*b}" if "d>0"
    73.9    using that
   73.10    by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
   73.11  
   73.12  lemma image_mult_atLeastAtMost_if:
   73.13 -  "( * ) c ` {x .. y} =
   73.14 +  "(*) c ` {x .. y} =
   73.15      (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
   73.16  proof -
   73.17    consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
   73.18 @@ -1028,7 +1028,7 @@
   73.19    then show ?thesis
   73.20    proof cases
   73.21      case 1
   73.22 -    have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
   73.23 +    have "(*) c ` {x .. y} = uminus ` (*) (- c) ` {x .. y}"
   73.24        by (simp add: image_image)
   73.25      also have "\<dots> = {c * y .. c * x}"
   73.26        using \<open>c < 0\<close>
   73.27 @@ -1049,7 +1049,7 @@
   73.28              else if 0 \<le> m then {m*a + c .. m *b + c}
   73.29              else {m*b + c .. m*a + c})"
   73.30  proof -
   73.31 -  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
   73.32 +  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o (*) m)"
   73.33      unfolding image_comp[symmetric]
   73.34      by (simp add: o_def)
   73.35    then show ?thesis
   73.36 @@ -2474,7 +2474,7 @@
   73.37  lemma prod_atLeastAtMost_code:
   73.38    "prod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
   73.39  proof -
   73.40 -  have "comp_fun_commute (\<lambda>a. ( * ) (f a))"
   73.41 +  have "comp_fun_commute (\<lambda>a. (*) (f a))"
   73.42      by unfold_locales (auto simp: o_def mult_ac)
   73.43    thus ?thesis
   73.44      by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)
    74.1 --- a/src/HOL/TLA/Intensional.thy	Sun Sep 23 21:49:31 2018 +0200
    74.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Sep 24 14:30:09 2018 +0200
    74.3 @@ -119,7 +119,7 @@
    74.4    "_liftIf"       == "_lift3 (CONST If)"
    74.5    "_liftPlus"     == "_lift2 (+)"
    74.6    "_liftMinus"    == "_lift2 (-)"
    74.7 -  "_liftTimes"    == "_lift2 (( * ))"
    74.8 +  "_liftTimes"    == "_lift2 ((*))"
    74.9    "_liftDiv"      == "_lift2 (div)"
   74.10    "_liftMod"      == "_lift2 (mod)"
   74.11    "_liftLess"     == "_lift2 (<)"
    75.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Sep 23 21:49:31 2018 +0200
    75.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 24 14:30:09 2018 +0200
    75.3 @@ -23,7 +23,7 @@
    75.4  val allowed_consts =
    75.5    [@{term "(+) :: int => _"}, @{term "(+) :: nat => _"},
    75.6     @{term "(-) :: int => _"}, @{term "(-) :: nat => _"},
    75.7 -   @{term "( * ) :: int => _"}, @{term "( * ) :: nat => _"},
    75.8 +   @{term "(*) :: int => _"}, @{term "(*) :: nat => _"},
    75.9     @{term "(div) :: int => _"}, @{term "(div) :: nat => _"},
   75.10     @{term "(mod) :: int => _"}, @{term "(mod) :: nat => _"},
   75.11     @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
   75.12 @@ -171,7 +171,7 @@
   75.13  val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP;
   75.14  
   75.15  val cadd =  @{cterm "(+) :: int => _"}
   75.16 -val cmulC =  @{cterm "( * ) :: int => _"}
   75.17 +val cmulC =  @{cterm "(*) :: int => _"}
   75.18  val cminus =  @{cterm "(-) :: int => _"}
   75.19  val cone =  @{cterm "1 :: int"}
   75.20  val [addC, mulC, subC] = map Thm.term_of [cadd, cmulC, cminus]
   75.21 @@ -662,7 +662,7 @@
   75.22    | term_of_num vs (Proc.Sub (t1, t2)) =
   75.23        @{term "(-) :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
   75.24    | term_of_num vs (Proc.Mul (i, t2)) =
   75.25 -      @{term "( * ) :: int => _"} $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2
   75.26 +      @{term "(*) :: int => _"} $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2
   75.27    | term_of_num vs (Proc.CN (n, i, t')) =
   75.28        term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
   75.29  
   75.30 @@ -765,7 +765,7 @@
   75.31    if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t))
   75.32    then false
   75.33    else case Thm.term_of t of
   75.34 -    c$l$r => if member (op =) [@{term"( * )::int => _"}, @{term"( * )::nat => _"}] c
   75.35 +    c$l$r => if member (op =) [@{term"(*)::int => _"}, @{term"(*)::nat => _"}] c
   75.36               then not (isnum l orelse isnum r)
   75.37               else not (member (op aconv) cts c)
   75.38    | c$_ => not (member (op aconv) cts c)
    76.1 --- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Sun Sep 23 21:49:31 2018 +0200
    76.2 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Mon Sep 24 14:30:09 2018 +0200
    76.3 @@ -61,13 +61,13 @@
    76.4  definition dependent :: "'b set \<Rightarrow> bool"
    76.5    where dependent_on_def: "dependent s \<longleftrightarrow> (\<exists>t u. finite t \<and> t \<subseteq> s \<and> (sum (\<lambda>v. u v *s v) t = 0 \<and> (\<exists>v\<in>t. u v \<noteq> 0)))"
    76.6  
    76.7 -lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 ( *s) = subspace"
    76.8 +lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 (*s) = subspace"
    76.9    unfolding subspace_on_def subspace_with_def ..
   76.10  
   76.11 -lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 ( *s) = dependent"
   76.12 +lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 (*s) = dependent"
   76.13    unfolding dependent_on_def dependent_with_def sum_with ..
   76.14  
   76.15 -lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 ( *s) = span"
   76.16 +lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 (*s) = span"
   76.17    unfolding span_on_def span_with_def sum_with ..
   76.18  
   76.19  end
   76.20 @@ -109,7 +109,7 @@
   76.21      then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V)
   76.22      else 0)"
   76.23  
   76.24 -lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 ( *s) = dim"
   76.25 +lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 (*s) = dim"
   76.26    unfolding dim_on_with_def dim_def implicit_ab_group_add ..
   76.27  
   76.28  end
    77.1 --- a/src/HOL/Vector_Spaces.thy	Sun Sep 23 21:49:31 2018 +0200
    77.2 +++ b/src/HOL/Vector_Spaces.thy	Mon Sep 24 14:30:09 2018 +0200
    77.3 @@ -77,10 +77,10 @@
    77.4  
    77.5  lemma linear_imp_scale:
    77.6    fixes D::"'a \<Rightarrow> 'b"
    77.7 -  assumes "linear ( *) scale D"
    77.8 +  assumes "linear (*) scale D"
    77.9    obtains d where "D = (\<lambda>x. scale x d)"
   77.10  proof -
   77.11 -  interpret linear "( *)" scale D by fact
   77.12 +  interpret linear "(*)" scale D by fact
   77.13    show ?thesis
   77.14      by (metis mult.commute mult.left_neutral scale that)
   77.15  qed
   77.16 @@ -806,7 +806,7 @@
   77.17  lemma in_span_in_range_construct:
   77.18    "x \<in> range (construct B f)" if i: "vs1.independent B" and x: "x \<in> vs2.span (f ` B)"
   77.19  proof -
   77.20 -  interpret linear "( *a)" "( *b)" "construct B f"
   77.21 +  interpret linear "(*a)" "(*b)" "construct B f"
   77.22      using i by (rule linear_construct)
   77.23    obtain bb :: "('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'b set \<Rightarrow> 'b" where
   77.24      "\<forall>x0 x1 x2. (\<exists>v4. v4 \<in> x2 \<and> x1 v4 \<noteq> x0 v4) = (bb x0 x1 x2 \<in> x2 \<and> x1 (bb x0 x1 x2) \<noteq> x0 (bb x0 x1 x2))"
   77.25 @@ -853,7 +853,7 @@
   77.26      have fB: "vs2.independent (f ` B)"
   77.27        using independent_injective_image[OF B f] .
   77.28      let ?g = "p.construct (f ` B) (the_inv_into B f)"
   77.29 -    show "linear ( *b) ( *a) ?g"
   77.30 +    show "linear (*b) (*a) ?g"
   77.31        by (rule p.linear_construct[OF fB])
   77.32      have "?g b \<in> vs1.span (the_inv_into B f ` f ` B)" for b
   77.33        by (intro p.construct_in_span fB)
   77.34 @@ -864,13 +864,13 @@
   77.35        by (auto simp: V_eq)
   77.36      have "(?g \<circ> f) v = id v" if "v \<in> vs1.span B" for v
   77.37      proof (rule vector_space_pair.linear_eq_on[where x=v])
   77.38 -      show "vector_space_pair ( *a) ( *a)" by unfold_locales
   77.39 -      show "linear ( *a) ( *a) (?g \<circ> f)"
   77.40 -      proof (rule Vector_Spaces.linear_compose[of _ "( *b)"])
   77.41 -        show "linear ( *a) ( *b) f"
   77.42 +      show "vector_space_pair (*a) (*a)" by unfold_locales
   77.43 +      show "linear (*a) (*a) (?g \<circ> f)"
   77.44 +      proof (rule Vector_Spaces.linear_compose[of _ "(*b)"])
   77.45 +        show "linear (*a) (*b) f"
   77.46            by unfold_locales
   77.47        qed fact
   77.48 -      show "linear ( *a) ( *a) id" by (rule vs1.linear_id)
   77.49 +      show "linear (*a) (*a) id" by (rule vs1.linear_id)
   77.50        show "v \<in> vs1.span B" by fact
   77.51        show "b \<in> B \<Longrightarrow> (p.construct (f ` B) (the_inv_into B f) \<circ> f) b = id b" for b
   77.52          by (simp add: p.construct_basis fB the_inv_into_f_f inj_on_subset[OF f vs1.span_superset])
   77.53 @@ -895,7 +895,7 @@
   77.54    proof (intro exI ballI conjI)
   77.55      interpret p: vector_space_pair s2 s1 by unfold_locales
   77.56      let ?g = "p.construct C g"
   77.57 -    show "linear ( *b) ( *a) ?g"
   77.58 +    show "linear (*b) (*a) ?g"
   77.59        by (rule p.linear_construct[OF C])
   77.60      have "?g v \<in> vs1.span (g ` C)" for v
   77.61        by (rule p.construct_in_span[OF C])
   77.62 @@ -903,10 +903,10 @@
   77.63      finally show "?g ` UNIV \<subseteq> V" by auto
   77.64      have "(f \<circ> ?g) v = id v" if v: "v \<in> f ` V" for v
   77.65      proof (rule vector_space_pair.linear_eq_on[where x=v])
   77.66 -      show "vector_space_pair ( *b) ( *b)" by unfold_locales
   77.67 -      show "linear ( *b) ( *b) (f \<circ> ?g)"
   77.68 -        by (rule Vector_Spaces.linear_compose[of _ "( *a)"]) fact+
   77.69 -      show "linear ( *b) ( *b) id" by (rule vs2.linear_id)
   77.70 +      show "vector_space_pair (*b) (*b)" by unfold_locales
   77.71 +      show "linear (*b) (*b) (f \<circ> ?g)"
   77.72 +        by (rule Vector_Spaces.linear_compose[of _ "(*a)"]) fact+
   77.73 +      show "linear (*b) (*b) id" by (rule vs2.linear_id)
   77.74        have "vs2.span (f ` B) = vs2.span C"
   77.75          using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
   77.76          by auto
    78.1 --- a/src/HOL/Word/Word.thy	Sun Sep 23 21:49:31 2018 +0200
    78.2 +++ b/src/HOL/Word/Word.thy	Mon Sep 24 14:30:09 2018 +0200
    78.3 @@ -273,7 +273,7 @@
    78.4  lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
    78.5    by (auto simp add: bintrunc_mod2p intro: mod_minus_cong)
    78.6  
    78.7 -lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "( * )"
    78.8 +lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(*)"
    78.9    by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
   78.10  
   78.11  definition word_div_def: "a div b = word_of_int (uint a div uint b)"
    79.1 --- a/src/HOL/ex/LocaleTest2.thy	Sun Sep 23 21:49:31 2018 +0200
    79.2 +++ b/src/HOL/ex/LocaleTest2.thy	Mon Sep 24 14:30:09 2018 +0200
    79.3 @@ -738,7 +738,7 @@
    79.4  
    79.5  
    79.6  locale Dgrp = Dmonoid +
    79.7 -  assumes unit [intro, simp]: "Dmonoid.unit (( ** )) one x"
    79.8 +  assumes unit [intro, simp]: "Dmonoid.unit ((**)) one x"
    79.9  
   79.10  begin
   79.11  
    80.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Sun Sep 23 21:49:31 2018 +0200
    80.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Mon Sep 24 14:30:09 2018 +0200
    80.3 @@ -38,7 +38,7 @@
    80.4  lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (+) (+)"
    80.5    unfolding rel_fun_def ZN_def by simp
    80.6  
    80.7 -lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (( * )) (( * ))"
    80.8 +lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) ((*)) ((*))"
    80.9    unfolding rel_fun_def ZN_def by simp
   80.10  
   80.11  definition tsub :: "int \<Rightarrow> int \<Rightarrow> int"
    81.1 --- a/src/Pure/Syntax/mixfix.ML	Sun Sep 23 21:49:31 2018 +0200
    81.2 +++ b/src/Pure/Syntax/mixfix.ML	Mon Sep 24 14:30:09 2018 +0200
    81.3 @@ -172,12 +172,8 @@
    81.4  val binder_name = suffix "_binder";
    81.5  
    81.6  fun mk_prefix sy =
    81.7 -  let
    81.8 -    fun star1 sys = (fst(hd sys) = "*");
    81.9 -    val sy' = Input.source_explode (Input.reset_pos sy); 
   81.10 -    val lpar = Symbol_Pos.explode0 ("'(" ^ (if star1 sy' then " " else ""));
   81.11 -    val rpar = Symbol_Pos.explode0 ((if star1(rev sy') then " " else "") ^ "')")
   81.12 - in lpar @ sy' @ rpar end
   81.13 +  let val sy' = Input.source_explode (Input.reset_pos sy); 
   81.14 +  in Symbol_Pos.explode0 "'(" @ sy' @ Symbol_Pos.explode0 "')" end
   81.15  
   81.16  fun syn_ext_consts logical_types const_decls =
   81.17    let