# HG changeset patch
# User nipkow
# Date 1537825783 -7200
# Node ID 5ed7206dbf184ff85a9d48de49027e91f4b4b919
# Parent  765ff343a7aa6dfa10fa8c696ec34ff40c2985f0# Parent  5f83db57e8c290d4f4b00cf182bb81fa6e8b1e42
merged

diff -r 765ff343a7aa -r 5ed7206dbf18 NEWS
--- a/NEWS	Mon Sep 24 22:10:24 2018 +0200
+++ b/NEWS	Mon Sep 24 23:49:43 2018 +0200
@@ -12,6 +12,9 @@
 * Old-style inner comments (* ... *) within the term language are no
 longer supported (legacy feature in Isabelle2018).
 
+* Infix operators that begin or end with a "*" can now be paranthesized
+without additional spaces, eg "(*)" instead of "( * )".
+
 
 *** Isar ***
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -443,9 +443,7 @@
 
   The alternative notation \<^verbatim>\<open>(\<close>\<open>sy\<close>\<^verbatim>\<open>)\<close> is introduced in addition. Thus any
   infix operator may be written in prefix form (as in Haskell), independently of
-  the number of arguments in the term. To avoid conflict with the comment brackets
-  \<^verbatim>\<open>(*\<close> and \<^verbatim>\<open>*)\<close>, infix operators that begin or end with a \<^verbatim>\<open>*\<close> require
-  extra spaces, e.g. \<^verbatim>\<open>( * )\<close>.
+  the number of arguments.
 \<close>
 
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Doc/Locales/Examples3.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -416,7 +416,7 @@
     using non_neg by unfold_locales (rule mult_left_mono)
 
 text \<open>While the proof of the previous interpretation
-  is straightforward from monotonicity lemmas for~@{term "( * )"}, the
+  is straightforward from monotonicity lemmas for~@{term "(*)"}, the
   second proof follows a useful pattern.\<close>
 
   sublocale %visible non_negative \<subseteq> lattice_end "(\<le>)" "\<lambda>i. n * i"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -339,7 +339,7 @@
 \begin{tabular}{@ {} lllllll @ {}}
 @{term "(+) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
 @{term "(-) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "( * ) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "(*) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
 @{term "(^) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
 @{term "(div) :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
 @{term "(mod) :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
@@ -367,7 +367,7 @@
 @{term "(+) :: int \<Rightarrow> int \<Rightarrow> int"} &
 @{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} &
 @{term "uminus :: int \<Rightarrow> int"} &
-@{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} &
 @{term "(^) :: int \<Rightarrow> nat \<Rightarrow> int"} &
 @{term "(div) :: int \<Rightarrow> int \<Rightarrow> int"}&
 @{term "(mod) :: int \<Rightarrow> int \<Rightarrow> int"}&
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -20,7 +20,7 @@
 subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
 
 abbreviation int_ring :: "int ring" ("\<Z>")
-  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
+  where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
 
 lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
   by simp
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Algebra/Sym_Groups.thy
--- a/src/HOL/Algebra/Sym_Groups.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Algebra/Sym_Groups.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -13,7 +13,7 @@
   where "sym_group n = \<lparr> carrier = { p. p permutes {1..n} }, mult = (\<circ>), one = id \<rparr>"
 
 definition sign_img :: "int monoid"
-  where "sign_img = \<lparr> carrier = { -1, 1 }, mult = ( * ), one = 1 \<rparr>"
+  where "sign_img = \<lparr> carrier = { -1, 1 }, mult = (*), one = 1 \<rparr>"
 
 
 lemma sym_group_is_group: "group (sym_group n)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1806,7 +1806,7 @@
 
 definition
   INTEG :: "int ring"
-  where "INTEG = \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
+  where "INTEG = \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
 
 lemma INTEG_cring: "cring INTEG"
   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Ball_Volume.thy
--- a/src/HOL/Analysis/Ball_Volume.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Ball_Volume.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -147,7 +147,7 @@
        (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
   also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
                (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
-               \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close>
+               \<partial>(distr lborel borel ((*) (1/r))))" using \<open>r > 0\<close>
     by (subst nn_integral_distr)
        (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
   also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) * 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1856,7 +1856,7 @@
 
   have sf[measurable]: "\<And>i. simple_function M (s' i)"
     unfolding s'_def using s(1)
-    by (intro simple_function_compose2[where h="( *\<^sub>R)"] simple_function_indicator) auto
+    by (intro simple_function_compose2[where h="(*\<^sub>R)"] simple_function_indicator) auto
 
   { fix i
     have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -697,7 +697,7 @@
   by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
 
 
-lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "( *\<^sub>R)"
+lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "(*\<^sub>R)"
   by (rule bounded_linear_scaleR_right)
 declare blinfun_scaleR_right.rep_eq[simp]
 
@@ -713,7 +713,7 @@
   by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
 
 
-lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "( * )"
+lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "(*)"
   by (rule bounded_linear_mult_right)
 declare blinfun_mult_right.rep_eq[simp]
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -203,7 +203,7 @@
 lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
   shows "matrix(adjoint f) = transpose(matrix f)"
 proof%unimportant -
-  have "matrix(adjoint f) = matrix(adjoint (( *v) (matrix f)))"
+  have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
     by (simp add: lf)
   also have "\<dots> = transpose(matrix f)"
     unfolding adjoint_matrix matrix_of_matrix_vector_mul
@@ -212,14 +212,14 @@
   finally show ?thesis .
 qed
 
-lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear (( *v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
+lemma%unimportant matrix_vector_mul_bounded_linear[intro, simp]: "bounded_linear ((*v) A)" for A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
   using matrix_vector_mul_linear[of A]
   by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
 
 lemma%unimportant (* FIX ME needs name*)
   fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
-  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
-    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
+  shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont ((*v) A) z"
+    and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S ((*v) A)"
   by (simp_all add: linear_continuous_at linear_continuous_on)
 
 lemma%unimportant scalar_invertible:
@@ -293,24 +293,24 @@
 
 lemma%important norm_column_le_onorm:
   fixes A :: "real^'n^'m"
-  shows "norm(column i A) \<le> onorm(( *v) A)"
+  shows "norm(column i A) \<le> onorm((*v) A)"
 proof%unimportant -
   have "norm (\<chi> j. A $ j $ i) \<le> norm (A *v axis i 1)"
     by (simp add: matrix_mult_dot cart_eq_inner_axis)
-  also have "\<dots> \<le> onorm (( *v) A)"
+  also have "\<dots> \<le> onorm ((*v) A)"
     using onorm [OF matrix_vector_mul_bounded_linear, of A "axis i 1"] by auto
-  finally have "norm (\<chi> j. A $ j $ i) \<le> onorm (( *v) A)" .
+  finally have "norm (\<chi> j. A $ j $ i) \<le> onorm ((*v) A)" .
   then show ?thesis
     unfolding column_def .
 qed
 
 lemma%important matrix_component_le_onorm:
   fixes A :: "real^'n^'m"
-  shows "\<bar>A $ i $ j\<bar> \<le> onorm(( *v) A)"
+  shows "\<bar>A $ i $ j\<bar> \<le> onorm((*v) A)"
 proof%unimportant -
   have "\<bar>A $ i $ j\<bar> \<le> norm (\<chi> n. (A $ n $ j))"
     by (metis (full_types, lifting) component_le_norm_cart vec_lambda_beta)
-  also have "\<dots> \<le> onorm (( *v) A)"
+  also have "\<dots> \<le> onorm ((*v) A)"
     by (metis (no_types) column_def norm_column_le_onorm)
   finally show ?thesis .
 qed
@@ -322,7 +322,7 @@
 
 lemma%important onorm_le_matrix_component_sum:
   fixes A :: "real^'n^'m"
-  shows "onorm(( *v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
+  shows "onorm((*v) A) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>A $ i $ j\<bar>)"
 proof%unimportant (rule onorm_le)
   fix x
   have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
@@ -345,7 +345,7 @@
 lemma%important onorm_le_matrix_component:
   fixes A :: "real^'n^'m"
   assumes "\<And>i j. abs(A$i$j) \<le> B"
-  shows "onorm(( *v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
+  shows "onorm((*v) A) \<le> real (CARD('m)) * real (CARD('n)) * B"
 proof%unimportant (rule onorm_le)
   fix x :: "real^'n::_"
   have "norm (A *v x) \<le> (\<Sum>i\<in>UNIV. \<bar>(A *v x) $ i\<bar>)"
@@ -403,13 +403,13 @@
     by (auto simp: lambda_skolem Bex_def)
   show ?thesis
   proof
-    have "onorm (( *v) (A - B)) \<le> real CARD('m) * real CARD('n) *
+    have "onorm ((*v) (A - B)) \<le> real CARD('m) * real CARD('n) *
     (e / (2 * real CARD('m) * real CARD('n)))"
       apply (rule onorm_le_matrix_component)
       using Bclo by (simp add: abs_minus_commute less_imp_le)
     also have "\<dots> < e"
       using \<open>0 < e\<close> by (simp add: divide_simps)
-    finally show "onorm (( *v) (A - B)) < e" .
+    finally show "onorm ((*v) (A - B)) < e" .
   qed (use B in auto)
 qed
 
@@ -778,7 +778,7 @@
     where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
 proof%unimportant -
   from assms obtain s where "finite s"
-    and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s"
+    and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s"
     by (rule cube_convex_hull)
   with that[of s] show thesis
     by (simp add: const_vector_cart)
@@ -982,11 +982,11 @@
       using basis_exists [of "span(rows A)"] by metis
     with span_subspace have eq: "span B = span(rows A)"
       by auto
-    then have inj: "inj_on (( *v) A) (span B)"
+    then have inj: "inj_on ((*v) A) (span B)"
       by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
-    then have ind: "independent (( *v) A ` B)"
+    then have ind: "independent ((*v) A ` B)"
       by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
-    have "dim (span (rows A)) \<le> card (( *v) A ` B)"
+    have "dim (span (rows A)) \<le> card ((*v) A ` B)"
       unfolding B(2)[symmetric]
       using inj
       by (auto simp: card_image inj_on_subset span_superset)
@@ -1017,7 +1017,7 @@
 
 lemma%unimportant columns_image_basis:
   fixes A :: "real^'n^'m"
-  shows "columns A = ( *v) A ` (range (\<lambda>i. axis i 1))"
+  shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
   by (force simp: columns_def matrix_vector_mult_basis [symmetric])
 
 lemma%important rank_dim_range:
@@ -1025,7 +1025,7 @@
   shows "rank A = dim(range (\<lambda>x. A *v x))"
   unfolding column_rank_def
 proof%unimportant (rule span_eq_dim)
-  have "span (columns A) \<subseteq> span (range (( *v) A))" (is "?l \<subseteq> ?r")
+  have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
     by (simp add: columns_image_basis image_subsetI span_mono)
   then show "?l = ?r"
     by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
@@ -1040,13 +1040,13 @@
 
 lemma%unimportant full_rank_injective:
   fixes A :: "real^'n^'m"
-  shows "rank A = CARD('n) \<longleftrightarrow> inj (( *v) A)"
+  shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
   by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
       dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
 
 lemma%unimportant full_rank_surjective:
   fixes A :: "real^'n^'m"
-  shows "rank A = CARD('m) \<longleftrightarrow> surj (( *v) A)"
+  shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
   by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
                 matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
 
@@ -1055,7 +1055,7 @@
 
 lemma%unimportant less_rank_noninjective:
   fixes A :: "real^'n^'m"
-  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj (( *v) A)"
+  shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
 using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
 
 lemma%unimportant matrix_nonfull_linear_equations_eq:
@@ -1071,7 +1071,7 @@
   fixes A :: "real^'n^'m" and B :: "real^'p^'n"
   shows "rank(A ** B) \<le> rank B"
 proof%unimportant -
-  have "rank(A ** B) \<le> dim (( *v) A ` range (( *v) B))"
+  have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
     by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
   also have "\<dots> \<le> rank B"
     by (simp add: rank_dim_range dim_image_le)
@@ -1137,7 +1137,7 @@
 
 lemma has_derivative_vector_1:
   assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
-  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' a))
+  shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a))
          (at ((vec a)::real^1) within vec ` S)"
     using der_g
     apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -20,7 +20,7 @@
   unfolding cart_basis_def Setcompr_eq_image
   by (rule card_image) (auto simp: inj_on_def axis_eq_axis)
 
-interpretation vec: vector_space "( *s) "
+interpretation vec: vector_space "(*s) "
   by unfold_locales (vector algebra_simps)+
 
 lemma%unimportant independent_cart_basis:
@@ -90,11 +90,11 @@
 qed
 
 (*Some interpretations:*)
-interpretation vec: finite_dimensional_vector_space "( *s)" "cart_basis"
+interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis"
   by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis)
 
 lemma%unimportant matrix_vector_mul_linear_gen[intro, simp]:
-  "Vector_Spaces.linear ( *s) ( *s) (( *v) A)"
+  "Vector_Spaces.linear (*s) (*s) ((*v) A)"
   by unfold_locales
     (vector matrix_vector_mult_def sum.distrib algebra_simps)+
 
@@ -108,10 +108,10 @@
 
 lemma%important linear_componentwise:
   fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
-  assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
+  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
   shows "(f x)$j = sum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
 proof%unimportant -
-  interpret lf: Vector_Spaces.linear "( *s)" "( *s)" f
+  interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f
     using lf .
   let ?M = "(UNIV :: 'm set)"
   let ?N = "(UNIV :: 'n set)"
@@ -123,13 +123,13 @@
     unfolding basis_expansion by auto
 qed
 
-interpretation vec: Vector_Spaces.linear "( *s)" "( *s)" "( *v) A"
+interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A"
   using matrix_vector_mul_linear_gen.
 
-interpretation vec: finite_dimensional_vector_space_pair "( *s)" cart_basis "( *s)" cart_basis ..
+interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis ..
 
 lemma%unimportant matrix_works:
-  assumes lf: "Vector_Spaces.linear ( *s) ( *s) f"
+  assumes lf: "Vector_Spaces.linear (*s) (*s) f"
   shows "matrix f *v x = f (x::'a::field ^ 'n)"
   apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
   apply clarify
@@ -140,8 +140,8 @@
   by (simp add: matrix_eq matrix_works)
 
 lemma%unimportant matrix_compose_gen:
-  assumes lf: "Vector_Spaces.linear ( *s) ( *s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
-    and lg: "Vector_Spaces.linear ( *s) ( *s) (g::'a^'m \<Rightarrow> 'a^_)"
+  assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
+    and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \<Rightarrow> 'a^_)"
   shows "matrix (g o f) = matrix g ** matrix f"
   using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]]
   by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
@@ -161,11 +161,11 @@
   by (metis matrix_transpose_mul transpose_mat transpose_transpose)
 
 lemma%unimportant linear_matrix_vector_mul_eq:
-  "Vector_Spaces.linear ( *s) ( *s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
+  "Vector_Spaces.linear (*s) (*s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
   by (simp add: scalar_mult_eq_scaleR linear_def)
 
 lemma%unimportant matrix_vector_mul[simp]:
-  "Vector_Spaces.linear ( *s) ( *s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
+  "Vector_Spaces.linear (*s) (*s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
   "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
   "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
   for f :: "real^'n \<Rightarrow> real ^'m"
@@ -173,20 +173,20 @@
 
 lemma%important matrix_left_invertible_injective:
   fixes A :: "'a::field^'n^'m"
-  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj (( *v) A)"
+  shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj ((*v) A)"
 proof%unimportant safe
   fix B
   assume B: "B ** A = mat 1"
-  show "inj (( *v) A)"
+  show "inj ((*v) A)"
     unfolding inj_on_def
       by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
 next
-  assume "inj (( *v) A)"
+  assume "inj ((*v) A)"
   from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
-  obtain g where "Vector_Spaces.linear ( *s) ( *s) g" and g: "g \<circ> ( *v) A = id"
+  obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
     by blast
   have "matrix g ** A = mat 1"
-    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear ( *s) ( *s) g\<close> g matrix_compose_gen
+    by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
         matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
   then show "\<exists>B. B ** A = mat 1"
     by metis
@@ -206,11 +206,11 @@
     { fix x :: "'a ^ 'm"
       have "A *v (B *v x) = x"
         by (simp add: matrix_vector_mul_assoc AB) }
-    hence "surj (( *v) A)" unfolding surj_def by metis }
+    hence "surj ((*v) A)" unfolding surj_def by metis }
   moreover
-  { assume sf: "surj (( *v) A)"
+  { assume sf: "surj ((*v) A)"
     from vec.linear_surjective_right_inverse[OF _ this]
-    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear ( *s) ( *s) g" "( *v) A \<circ> g = id"
+    obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
       by blast
 
     have "A ** (matrix g) = mat 1"
@@ -339,11 +339,11 @@
 proof%unimportant -
   { fix A A' :: "'a ^'n^'n"
     assume AA': "A ** A' = mat 1"
-    have sA: "surj (( *v) A)"
+    have sA: "surj ((*v) A)"
       using AA' matrix_right_invertible_surjective by auto
     from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
     obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
-      where f': "Vector_Spaces.linear ( *s) ( *s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
+      where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
     have th: "matrix f' ** A = mat 1"
       by (simp add: matrix_eq matrix_works[OF f'(1)]
           matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
@@ -448,13 +448,13 @@
   finally show ?thesis .
 qed
 
-interpretation vector_space_over_itself: vector_space "( *) :: 'a::field => 'a => 'a"
+interpretation vector_space_over_itself: vector_space "(*) :: 'a::field => 'a => 'a"
   by unfold_locales (simp_all add: algebra_simps)
 
 lemmas [simp del] = vector_space_over_itself.scale_scale
 
 interpretation vector_space_over_itself: finite_dimensional_vector_space
-  "( *) :: 'a::field => 'a => 'a" "{1}"
+  "(*) :: 'a::field => 'a => 'a" "{1}"
   by unfold_locales (auto simp: vector_space_over_itself.span_singleton)
 
 lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -228,7 +228,7 @@
 
 lemma continuous_on_joinpaths_D1:
     "continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1"
-  apply (rule continuous_on_eq [of _ "(g1 +++ g2) \<circ> (( *)(inverse 2))"])
+  apply (rule continuous_on_eq [of _ "(g1 +++ g2) \<circ> ((*)(inverse 2))"])
   apply (rule continuous_intros | simp)+
   apply (auto elim!: continuous_on_subset simp: joinpaths_def)
   done
@@ -251,13 +251,13 @@
   show ?thesis
     unfolding piecewise_differentiable_on_def
   proof (intro exI conjI ballI cont)
-    show "finite (insert 1 ((( *)2) ` S))"
+    show "finite (insert 1 (((*)2) ` S))"
       by (simp add: \<open>finite S\<close>)
-    show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
+    show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
     proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
       have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}"
         by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
-      then show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x within {0..1}"
+      then show "g1 +++ g2 \<circ> (*) (inverse 2) differentiable at x within {0..1}"
         by (auto intro: differentiable_chain_within)
     qed (use that in \<open>auto simp: joinpaths_def\<close>)
   qed
@@ -598,49 +598,49 @@
              and co12: "continuous_on ({0..1} - S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
              and g12D: "\<forall>x\<in>{0..1} - S. g1 +++ g2 differentiable at x"
     using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
-  have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
+  have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
   proof (rule differentiable_transform_within)
-    show "g1 +++ g2 \<circ> ( *) (inverse 2) differentiable at x"
+    show "g1 +++ g2 \<circ> (*) (inverse 2) differentiable at x"
       using that g12D
       apply (simp only: joinpaths_def)
       by (rule differentiable_chain_at derivative_intros | force)+
     show "\<And>x'. \<lbrakk>dist x' x < dist (x/2) (1/2)\<rbrakk>
-          \<Longrightarrow> (g1 +++ g2 \<circ> ( *) (inverse 2)) x' = g1 x'"
+          \<Longrightarrow> (g1 +++ g2 \<circ> (*) (inverse 2)) x' = g1 x'"
       using that by (auto simp: dist_real_def joinpaths_def)
   qed (use that in \<open>auto simp: dist_real_def\<close>)
-  have [simp]: "vector_derivative (g1 \<circ> ( *) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
-               if "x \<in> {0..1} - insert 1 (( *) 2 ` S)" for x
+  have [simp]: "vector_derivative (g1 \<circ> (*) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
+               if "x \<in> {0..1} - insert 1 ((*) 2 ` S)" for x
     apply (subst vector_derivative_chain_at)
     using that
     apply (rule derivative_eq_intros g1D | simp)+
     done
   have "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
     using co12 by (rule continuous_on_subset) force
-  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 \<circ> ( *)2) (at x))"
+  then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (\<lambda>x. vector_derivative (g1 \<circ> (*)2) (at x))"
   proof (rule continuous_on_eq [OF _ vector_derivative_at])
-    show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \<circ> ( *) 2) (at x)) (at x)"
+    show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 \<circ> (*) 2) (at x)) (at x)"
       if "x \<in> {0..1/2} - insert (1/2) S" for x
     proof (rule has_vector_derivative_transform_within)
-      show "(g1 \<circ> ( *) 2 has_vector_derivative vector_derivative (g1 \<circ> ( *) 2) (at x)) (at x)"
+      show "(g1 \<circ> (*) 2 has_vector_derivative vector_derivative (g1 \<circ> (*) 2) (at x)) (at x)"
         using that
         by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric])
-      show "\<And>x'. \<lbrakk>dist x' x < dist x (1/2)\<rbrakk> \<Longrightarrow> (g1 \<circ> ( *) 2) x' = (g1 +++ g2) x'"
+      show "\<And>x'. \<lbrakk>dist x' x < dist x (1/2)\<rbrakk> \<Longrightarrow> (g1 \<circ> (*) 2) x' = (g1 +++ g2) x'"
         using that by (auto simp: dist_norm joinpaths_def)
     qed (use that in \<open>auto simp: dist_norm\<close>)
   qed
-  have "continuous_on ({0..1} - insert 1 (( *) 2 ` S))
-                      ((\<lambda>x. 1/2 * vector_derivative (g1 \<circ> ( *)2) (at x)) \<circ> ( *)(1/2))"
+  have "continuous_on ({0..1} - insert 1 ((*) 2 ` S))
+                      ((\<lambda>x. 1/2 * vector_derivative (g1 \<circ> (*)2) (at x)) \<circ> (*)(1/2))"
     apply (rule continuous_intros)+
     using coDhalf
     apply (simp add: scaleR_conv_of_real image_set_diff image_image)
     done
-  then have con_g1: "continuous_on ({0..1} - insert 1 (( *) 2 ` S)) (\<lambda>x. vector_derivative g1 (at x))"
+  then have con_g1: "continuous_on ({0..1} - insert 1 ((*) 2 ` S)) (\<lambda>x. vector_derivative g1 (at x))"
     by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
   have "continuous_on {0..1} g1"
     using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
   with \<open>finite S\<close> show ?thesis
     apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
-    apply (rule_tac x="insert 1 ((( *)2)`S)" in exI)
+    apply (rule_tac x="insert 1 (((*)2)`S)" in exI)
     apply (simp add: g1D con_g1)
   done
 qed
@@ -959,7 +959,7 @@
     apply (rule piecewise_C1_differentiable_compose)
     using assms
     apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
-    apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
+    apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
     done
   moreover have "(g2 \<circ> (\<lambda>x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
     apply (rule piecewise_C1_differentiable_compose)
@@ -1030,9 +1030,9 @@
     apply (auto simp: algebra_simps vector_derivative_works)
     done
   have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
-    apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (( *)2 -` s1)"])
+    apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) ((*)2 -` s1)"])
     using s1
-    apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
+    apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
     apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
     done
   moreover have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
@@ -1608,7 +1608,7 @@
       by (simp add: has_vector_derivative_def scaleR_conv_of_real)
     have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
       using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
-    then have fdiff: "(f has_derivative ( *) (f' (g x))) (at (g x) within g ` {a..b})"
+    then have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {a..b})"
       by (simp add: has_field_derivative_def)
     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})"
       using diff_chain_within [OF gdiff fdiff]
@@ -6158,9 +6158,9 @@
   case 0 then show ?case by simp
 next
   case (Suc n z)
-  have holo0: "f holomorphic_on ( *) u ` S"
+  have holo0: "f holomorphic_on (*) u ` S"
     by (meson fg f holomorphic_on_subset image_subset_iff)
-  have holo2: "(deriv ^^ n) f holomorphic_on ( * ) u ` S"
+  have holo2: "(deriv ^^ n) f holomorphic_on (*) u ` S"
     by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
   have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on S"
     by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
@@ -6182,7 +6182,7 @@
     apply (blast intro: fg)
     done
   also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
-      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "( *) u", unfolded o_def])
+      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "(*) u", unfolded o_def])
       apply (rule derivative_intros)
       using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv T apply blast
       apply (simp add: deriv_linear)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -186,7 +186,7 @@
 qed
 
 lemma%unimportant matrix_vector_mult_matrix_matrix_mult_compose:
-  "( *v) (A ** B) = ( *v) A \<circ> ( *v) B"
+  "(*v) (A ** B) = (*v) A \<circ> (*v) B"
   by (auto simp: matrix_vector_mul_assoc)
 
 lemma%unimportant induct_linear_elementary:
@@ -199,17 +199,17 @@
     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)"
   shows "P f"
 proof -
-  have "P (( *v) A)" for A
+  have "P ((*v) A)" for A
   proof (rule induct_matrix_elementary_alt)
     fix A B
-    assume "P (( *v) A)" and "P (( *v) B)"
-    then show "P (( *v) (A ** B))"
+    assume "P ((*v) A)" and "P ((*v) B)"
+    then show "P ((*v) (A ** B))"
       by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
           intro!: comp)
   next
     fix A :: "real^'n^'n" and i
     assume "row i A = 0"
-    show "P (( *v) A)"
+    show "P ((*v) A)"
       using matrix_vector_mul_linear
       by (rule zeroes[where i=i])
         (metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta)
@@ -218,9 +218,9 @@
     assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
     have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
       by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
-    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = (( *v) A)"
+    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = ((*v) A)"
       by (auto simp: 0 matrix_vector_mult_def)
-    then show "P (( *v) A)"
+    then show "P ((*v) A)"
       using const [of "\<lambda>i. A $ i $ i"] by simp
   next
     fix m n :: "'n"
@@ -229,9 +229,9 @@
               (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
       for i and x :: "real^'n"
       unfolding swap_def by (rule sum.cong) auto
-    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))"
+    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))"
       by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
-    with swap [OF \<open>m \<noteq> n\<close>] show "P (( *v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
+    with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
       by (simp add: mat_def matrix_vector_mult_def)
   next
     fix m n :: "'n"
@@ -239,10 +239,10 @@
     then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
       by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
     then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
-               (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
+               ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
       unfolding matrix_vector_mult_def of_bool_def
       by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
-    then show "P (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
+    then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
       using idplus [OF \<open>m \<noteq> n\<close>] by simp
   qed
   then show ?thesis
@@ -1496,21 +1496,21 @@
                 \<le> sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}"
             by (rule sum_mono) (simp add: indicator_def divide_simps)
         next
-          have \<alpha>: "?a = (\<Sum>k \<in> ( *)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
+          have \<alpha>: "?a = (\<Sum>k \<in> (*)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
                          k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
             by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
           have \<beta>: "sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
                    = (\<Sum>k \<in> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
                       k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
             by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
-          have 0: "( *) 2 ` {k \<in> \<int>. P k} \<inter> (\<lambda>x. 2 * x + 1) ` {k \<in> \<int>. P k} = {}" for P :: "real \<Rightarrow> bool"
+          have 0: "(*) 2 ` {k \<in> \<int>. P k} \<inter> (\<lambda>x. 2 * x + 1) ` {k \<in> \<int>. P k} = {}" for P :: "real \<Rightarrow> bool"
           proof -
             have "2 * i \<noteq> 2 * j + 1" for i j :: int by arith
             thus ?thesis
               unfolding Ints_def by auto (use of_int_eq_iff in fastforce)
           qed
           have "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
-                = (\<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)}.
+                = (\<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)}.
                   k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
             unfolding \<alpha> \<beta>
             using finite_abs_int_segment [of "2 ^ (2*n)"]
@@ -1519,7 +1519,7 @@
           proof (rule sum_mono2)
             show "finite {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
               by (rule finite_abs_int_segment)
-            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)}"
+            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)}"
               apply auto
               using one_le_power [of "2::real" "2*n"]  by linarith
             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
@@ -1535,7 +1535,7 @@
             qed
             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"
                   if "b \<in> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)} -
-                          (( *) 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
+                          ((*) 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
               using that by (simp add: indicator_def divide_simps)
           qed
           finally show "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<le> ?b" .
@@ -2121,8 +2121,8 @@
           moreover
           interpret linear "f' x" by fact
           have "(matrix (f' x) - B) *v w = 0" for w
-          proof (rule lemma_partial_derivatives [of "( *v) (matrix (f' x) - B)"])
-            show "linear (( *v) (matrix (f' x) - B))"
+          proof (rule lemma_partial_derivatives [of "(*v) (matrix (f' x) - B)"])
+            show "linear ((*v) (matrix (f' x) - B))"
               by (rule matrix_vector_mul_linear)
             have "((\<lambda>y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
               using tendsto_minus [OF lim_df] by (simp add: algebra_simps divide_simps)
@@ -2141,19 +2141,19 @@
                   proof (rule eventually_sequentiallyI)
                     fix k :: "nat"
                     assume "0 \<le> k"
-                    have "0 \<le> onorm (( *v) (A k - B))"
+                    have "0 \<le> onorm ((*v) (A k - B))"
                       using matrix_vector_mul_bounded_linear
                       by (rule onorm_pos_le)
-                    then show "norm (onorm (( *v) (A k - B))) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>(A k - B) $ i $ j\<bar>)"
+                    then show "norm (onorm ((*v) (A k - B))) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>(A k - B) $ i $ j\<bar>)"
                       by (simp add: onorm_le_matrix_component_sum del: vector_minus_component)
                   qed
                 next
                   show "?g \<longlonglongrightarrow> 0"
                     using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: tendsto_null_sum)
                 qed
-                with \<open>e > 0\<close> obtain p where "\<And>n. n \<ge> p \<Longrightarrow> \<bar>onorm (( *v) (A n - B))\<bar> < e/2"
+                with \<open>e > 0\<close> obtain p where "\<And>n. n \<ge> p \<Longrightarrow> \<bar>onorm ((*v) (A n - B))\<bar> < e/2"
                   unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral)
-                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`]*)
+                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`]*)
                   using le_add1 by blast
                 show "\<exists>d>0. \<forall>y\<in>S. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow>
                            inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e"
@@ -2196,12 +2196,12 @@
                 by (simp add: algebra_simps diff lin_df matrix_vector_mul_linear scalar_mult_eq_scaleR)
             qed
           qed (use x in \<open>simp; auto simp: not_less\<close>)
-          ultimately have "f' x = ( *v) B"
+          ultimately have "f' x = (*v) B"
             by (force simp: algebra_simps scalar_mult_eq_scaleR)
           show "matrix (f' x) $ m $ n \<le> b"
           proof (rule tendsto_upperbound [of "\<lambda>i. (A i $ m $ n)" _ sequentially])
             show "(\<lambda>i. A i $ m $ n) \<longlonglongrightarrow> matrix (f' x) $ m $ n"
-              by (simp add: B \<open>f' x = ( *v) B\<close>)
+              by (simp add: B \<open>f' x = (*v) B\<close>)
             show "\<forall>\<^sub>F i in sequentially. A i $ m $ n \<le> b"
               by (simp add: Ab less_eq_real_def)
           qed auto
@@ -2214,7 +2214,7 @@
             using f [OF \<open>x \<in> S\<close>] unfolding Deriv.has_derivative_at_within Lim_within
             by (auto simp: field_simps dest: spec [of _ "e/2"])
           let ?A = "matrix(f' x) - (\<chi> i j. if i = m \<and> j = n then e / 4 else 0)"
-          obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm(( *v) (?A - B)) < e/6"
+          obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm((*v) (?A - B)) < e/6"
             using matrix_rational_approximation \<open>e > 0\<close>
             by (metis zero_less_divide_iff zero_less_numeral)
           show "\<exists>d>0. \<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and>
@@ -2224,7 +2224,7 @@
               by (rule \<open>d>0\<close>)
             show "B $ m $ n < b"
             proof -
-              have "\<bar>matrix (( *v) (?A - B)) $ m $ n\<bar> \<le> onorm (( *v) (?A - B))"
+              have "\<bar>matrix ((*v) (?A - B)) $ m $ n\<bar> \<le> onorm ((*v) (?A - B))"
                 using component_le_onorm [OF matrix_vector_mul_linear, of _ m n] by metis
               then show ?thesis
                 using b Bo_e6 by simp
@@ -3805,12 +3805,12 @@
   let ?drop = "(\<lambda>x::real^1. x $ 1)"
   have S': "?lift ` S \<in> sets lebesgue"
     by (auto intro: differentiable_image_in_sets_lebesgue [OF S] differentiable_vec)
-  have "((\<lambda>x. vec (g (x $ 1))) has_derivative ( *\<^sub>R) (g' z)) (at (vec z) within ?lift ` S)"
+  have "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' z)) (at (vec z) within ?lift ` S)"
     if "z \<in> S" for z
     using der_g [OF that]
     by (simp add: has_vector_derivative_def has_derivative_vector_1)
   then have der': "\<And>x. x \<in> ?lift ` S \<Longrightarrow>
-        (?lift \<circ> g \<circ> ?drop has_derivative ( *\<^sub>R) (g' (?drop x))) (at x within ?lift ` S)"
+        (?lift \<circ> g \<circ> ?drop has_derivative (*\<^sub>R) (g' (?drop x))) (at x within ?lift ` S)"
     by (auto simp: o_def)
   have inj': "inj_on (vec \<circ> g \<circ> ?drop) (vec ` S)"
     using inj by (simp add: inj_on_def)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -16,7 +16,7 @@
 
 lemma has_derivative_mult_right:
   fixes c:: "'a :: real_normed_algebra"
-  shows "((( * ) c) has_derivative (( * ) c)) F"
+  shows "(((*) c) has_derivative ((*) c)) F"
 by (rule has_derivative_mult_right [OF has_derivative_ident])
 
 lemma has_derivative_of_real[derivative_intros, simp]:
@@ -25,7 +25,7 @@
 
 lemma has_vector_derivative_real_field:
   "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
-  using has_derivative_compose[of of_real of_real a _ f "( * ) f'"]
+  using has_derivative_compose[of of_real of_real a _ f "(*) f'"]
   by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
 lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
 
@@ -59,10 +59,10 @@
   shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
   using assms by (intro vector_derivative_cnj_within) auto
 
-lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
+lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
   by auto
 
-lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
+lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
   by auto
 
 lemma uniformly_continuous_on_cmul_right [continuous_intros]:
@@ -283,7 +283,7 @@
 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"
   by (metis holomorphic_transform)
 
-lemma holomorphic_on_linear [simp, holomorphic_intros]: "(( * ) c) holomorphic_on s"
+lemma holomorphic_on_linear [simp, holomorphic_intros]: "((*) c) holomorphic_on s"
   unfolding holomorphic_on_def by (metis field_differentiable_linear)
 
 lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
@@ -572,7 +572,7 @@
   finally show ?thesis .
 qed
 
-lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on S"
+lemma analytic_on_linear [analytic_intros,simp]: "((*) c) analytic_on S"
   by (auto simp add: analytic_on_holomorphic)
 
 lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on S"
@@ -905,9 +905,9 @@
     by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
   then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
     "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
-  from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
+  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
     by (simp add: has_field_derivative_def S)
-  have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
+  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
     by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
        (insert g, auto simp: sums_iff)
   thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1133,10 +1133,10 @@
       done
     with \<open>e>0\<close> show ?thesis by force
   qed
-  have "inj (( * ) (deriv f \<xi>))"
+  have "inj ((*) (deriv f \<xi>))"
     using dnz by simp
-  then obtain g' where g': "linear g'" "g' \<circ> ( * ) (deriv f \<xi>) = id"
-    using linear_injective_left_inverse [of "( * ) (deriv f \<xi>)"]
+  then obtain g' where g': "linear g'" "g' \<circ> (*) (deriv f \<xi>) = id"
+    using linear_injective_left_inverse [of "(*) (deriv f \<xi>)"]
     by (auto simp: linear_times)
   show ?thesis
     apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g'])
@@ -2083,10 +2083,10 @@
     apply (simp add: C_def False fo)
     apply (simp add: derivative_intros dfa complex_derivative_chain)
     done
-  have sb1: "( * ) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
+  have sb1: "(*) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
              \<subseteq> f ` ball a r"
     using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
-  have sb2: "ball (C * r * b) r' \<subseteq> ( * ) (C * r) ` ball b t"
+  have sb2: "ball (C * r * b) r' \<subseteq> (*) (C * r) ` ball b t"
              if "1 / 12 < t" for b t
   proof -
     have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Connected.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -2257,14 +2257,14 @@
         unfolding dist_norm
         using norm_scaleR[of c "(1 / c) *\<^sub>R y - x", unfolded scaleR_right_diff_distrib, unfolded scaleR_scaleR] assms(1)
           assms(1)[unfolded zero_less_abs_iff[symmetric]] by (simp del:zero_less_abs_iff)
-      then have "y \<in> ( *\<^sub>R) c ` s"
-        using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "( *\<^sub>R) c"]
+      then have "y \<in> (*\<^sub>R) c ` s"
+        using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "(*\<^sub>R) c"]
         using e[THEN spec[where x="(1 / c) *\<^sub>R y"]]
         using assms(1)
         unfolding dist_norm scaleR_scaleR
         by auto
     }
-    ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> ( *\<^sub>R) c ` s"
+    ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> (*\<^sub>R) c ` s"
       apply (rule_tac x="e * \<bar>c\<bar>" in exI, auto)
       done
   }
@@ -2311,10 +2311,10 @@
 proof -
   have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)"
     unfolding o_def ..
-  have "(+) a ` ( *\<^sub>R) c ` S = ((+) a \<circ> ( *\<^sub>R) c) ` S"
+  have "(+) a ` (*\<^sub>R) c ` S = ((+) a \<circ> (*\<^sub>R) c) ` S"
     by auto
   then show ?thesis
-    using assms open_translation[of "( *\<^sub>R) c ` S" a]
+    using assms open_translation[of "(*\<^sub>R) c ` S" a]
     unfolding *
     by auto
 qed
@@ -2637,7 +2637,7 @@
   assumes "compact s"
   shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof -
-  have "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
+  have "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
     by auto
   then show ?thesis
     using compact_translation[OF compact_scaling[OF assms], of a c] by auto
@@ -3719,7 +3719,7 @@
   assumes "c \<noteq> 0"
   shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
 proof -
-  have *: "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
+  have *: "(+) a ` (*\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
   show ?thesis
     using homeomorphic_trans
     using homeomorphic_scaling[OF assms, of s]
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -664,7 +664,7 @@
   assumes "convex S"
   shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)"
 proof -
-  have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` ( *\<^sub>R) c ` S"
+  have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S"
     by auto
   then show ?thesis
     using convex_translation[OF convex_scaling[OF assms], of a c] by auto
@@ -1229,12 +1229,12 @@
 
 lemma closure_scaleR:
   fixes S :: "'a::real_normed_vector set"
-  shows "(( *\<^sub>R) c) ` (closure S) = closure ((( *\<^sub>R) c) ` S)"
+  shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
 proof
-  show "(( *\<^sub>R) c) ` (closure S) \<subseteq> closure ((( *\<^sub>R) c) ` S)"
+  show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
     using bounded_linear_scaleR_right
     by (rule closure_bounded_linear_image_subset)
-  show "closure ((( *\<^sub>R) c) ` S) \<subseteq> (( *\<^sub>R) c) ` (closure S)"
+  show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
     by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
 qed
 
@@ -1945,7 +1945,7 @@
 
 lemma cone_iff:
   assumes "S \<noteq> {}"
-  shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
+  shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
 proof -
   {
     assume "cone S"
@@ -1955,7 +1955,7 @@
       {
         fix x
         assume "x \<in> S"
-        then have "x \<in> (( *\<^sub>R) c) ` S"
+        then have "x \<in> ((*\<^sub>R) c) ` S"
           unfolding image_def
           using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"]
             exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
@@ -1964,19 +1964,19 @@
       moreover
       {
         fix x
-        assume "x \<in> (( *\<^sub>R) c) ` S"
+        assume "x \<in> ((*\<^sub>R) c) ` S"
         then have "x \<in> S"
           using \<open>cone S\<close> \<open>c > 0\<close>
           unfolding cone_def image_def \<open>c > 0\<close> by auto
       }
-      ultimately have "(( *\<^sub>R) c) ` S = S" by auto
+      ultimately have "((*\<^sub>R) c) ` S = S" by auto
     }
-    then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
+    then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
       using \<open>cone S\<close> cone_contains_0[of S] assms by auto
   }
   moreover
   {
-    assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
+    assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
     {
       fix x
       assume "x \<in> S"
@@ -2061,9 +2061,9 @@
   then show ?thesis by auto
 next
   case False
-  then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
+  then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
     using cone_iff[of S] assms by auto
-  then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` closure S = closure S)"
+  then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
     using closure_subset by (auto simp: closure_scaleR)
   then show ?thesis
     using False cone_iff[of "closure S"] by auto
@@ -5705,19 +5705,19 @@
   then show ?thesis by auto
 next
   case False
-  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
+  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
     using cone_iff[of S] assms by auto
   {
     fix c :: real
     assume "c > 0"
-    then have "( *\<^sub>R) c ` (convex hull S) = convex hull (( *\<^sub>R) c ` S)"
+    then have "(*\<^sub>R) c ` (convex hull S) = convex hull ((*\<^sub>R) c ` S)"
       using convex_hull_scaling[of _ S] by auto
     also have "\<dots> = convex hull S"
       using * \<open>c > 0\<close> by auto
-    finally have "( *\<^sub>R) c ` (convex hull S) = convex hull S"
+    finally have "(*\<^sub>R) c ` (convex hull S) = convex hull S"
       by auto
   }
-  then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> (( *\<^sub>R) c ` (convex hull S)) = (convex hull S)"
+  then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> ((*\<^sub>R) c ` (convex hull S)) = (convex hull S)"
     using * hull_subset[of S convex] by auto
   then show ?thesis
     using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto
@@ -6403,7 +6403,7 @@
     assume "y \<in> cbox (x - ?d) (x + ?d)"
     then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
       using assms by (simp add: mem_box field_simps inner_simps)
-    with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
+    with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum ((*\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
       by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
   next
     fix y
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -52,7 +52,7 @@
 lemma has_derivative_right:
   fixes f :: "real \<Rightarrow> real"
     and y :: "real"
-  shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
+  shows "(f has_derivative ((*) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
          ((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
 proof -
   have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
@@ -983,7 +983,7 @@
   assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
   shows   "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
 proof (rule has_derivative_zero_constant)
-  have A: "( * ) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
+  have A: "(*) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
   fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
     using assms(2)[of x] by (simp add: has_field_derivative_def A)
 qed fact
@@ -1911,9 +1911,9 @@
   then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
     "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
   from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
-  from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
+  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
     by (simp add: has_field_derivative_def S)
-  have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
+  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
     by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
        (insert g, auto simp: sums_iff)
   thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
@@ -2218,7 +2218,7 @@
   unfolding field_differentiable_def
   by (metis DERIV_subset top_greatest)
 
-lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F"
+lemma field_differentiable_linear [simp,derivative_intros]: "((*) c) field_differentiable F"
   unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
   by (force intro: has_derivative_mult_right)
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -452,7 +452,7 @@
 lemma%unimportant  matrix_id [simp]: "det (matrix id) = 1"
   by (simp add: matrix_id_mat_1)
 
-lemma%important  det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
+lemma%important  det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
   apply (subst det_diagonal)
    apply (auto simp: matrix_def mat_def)
   apply (simp add: cart_eq_inner_axis inner_axis_axis)
@@ -750,7 +750,7 @@
 
 lemma%unimportant  det_nz_iff_inj_gen:
   fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n"
-  assumes "Vector_Spaces.linear ( *s) ( *s) f"
+  assumes "Vector_Spaces.linear (*s) (*s) f"
   shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
 proof
   assume "det (matrix f) \<noteq> 0"
@@ -780,22 +780,22 @@
 
 lemma%important  matrix_left_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
-  assumes "Vector_Spaces.linear ( *s) ( *s) f"
-  shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id))"
+  assumes "Vector_Spaces.linear (*s) (*s) f"
+  shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id))"
 proof%unimportant safe
   fix B
   assume 1: "B ** matrix f = mat 1"
-  show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
+  show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id"
   proof (intro exI conjI)
-    show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)"
+    show "Vector_Spaces.linear (*s) (*s) (\<lambda>y. B *v y)"
       by simp
-    show "(( *v) B) \<circ> f = id"
+    show "((*v) B) \<circ> f = id"
       unfolding o_def
       by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid)
   qed
 next
   fix g
-  assume "Vector_Spaces.linear ( *s) ( *s) g" "g \<circ> f = id"
+  assume "Vector_Spaces.linear (*s) (*s) g" "g \<circ> f = id"
   then have "matrix g ** matrix f = mat 1"
     by (metis assms matrix_compose_gen matrix_id_mat_1)
   then show "\<exists>B. B ** matrix f = mat 1" ..
@@ -808,22 +808,22 @@
 
 lemma%unimportant  matrix_right_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a^'n"
-  assumes "Vector_Spaces.linear ( *s) ( *s) f"
-  shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id))"
+  assumes "Vector_Spaces.linear (*s) (*s) f"
+  shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id))"
 proof safe
   fix B
   assume 1: "matrix f ** B = mat 1"
-  show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id"
+  show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id"
   proof (intro exI conjI)
-    show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)"
+    show "Vector_Spaces.linear (*s) (*s) ((*v) B)"
       by simp
-    show "f \<circ> ( *v) B = id"
+    show "f \<circ> (*v) B = id"
       using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
       by (metis (no_types, hide_lams))
   qed
 next
   fix g
-  assume "Vector_Spaces.linear ( *s) ( *s) g" and "f \<circ> g = id"
+  assume "Vector_Spaces.linear (*s) (*s) g" and "f \<circ> g = id"
   then have "matrix f ** matrix g = mat 1"
     by (metis assms matrix_compose_gen matrix_id_mat_1)
   then show "\<exists>B. matrix f ** B = mat 1" ..
@@ -836,8 +836,8 @@
 
 lemma%unimportant  matrix_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
-  assumes "Vector_Spaces.linear ( *s) ( *s) f"
-  shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
+  assumes "Vector_Spaces.linear (*s) (*s) f"
+  shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
     (is "?lhs = ?rhs")
 proof
   assume ?lhs then show ?rhs
@@ -855,7 +855,7 @@
 
 lemma%unimportant  invertible_eq_bij:
   fixes m :: "'a::field^'m^'n"
-  shows "invertible m \<longleftrightarrow> bij (( *v) m)"
+  shows "invertible m \<longleftrightarrow> bij ((*v) m)"
   using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul]
   by (metis bij_betw_def left_right_inverse_eq matrix_vector_mul_linear_gen o_bij
       vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
@@ -1028,7 +1028,7 @@
   let ?m1 = "mat 1 :: real ^'n^'n"
   {
     assume ot: ?ot
-    from ot have lf: "Vector_Spaces.linear ( *s) ( *s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
+    from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
       unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR
       by blast+
     {
@@ -1052,7 +1052,7 @@
   }
   moreover
   {
-    assume lf: "Vector_Spaces.linear ( *s) ( *s) f" and om: "orthogonal_matrix ?mf"
+    assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
     from lf om have ?lhs
       unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
       apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -307,7 +307,7 @@
 subsection \<open>Locale instances\<close>
 
 lemma finite_dimensional_vector_space_euclidean:
-  "finite_dimensional_vector_space ( *\<^sub>R) Basis"
+  "finite_dimensional_vector_space (*\<^sub>R) Basis"
 proof unfold_locales
   show "finite (Basis::'a set)" by (metis finite_Basis)
   show "real_vector.independent (Basis::'a set)"
@@ -318,20 +318,20 @@
     apply (drule_tac f="inner a" in arg_cong)
     apply (simp add: inner_Basis inner_sum_right eq_commute)
     done
-  show "module.span ( *\<^sub>R) Basis = UNIV"
+  show "module.span (*\<^sub>R) Basis = UNIV"
     unfolding span_finite [OF finite_Basis] span_raw_def[symmetric]
     by (auto intro!: euclidean_representation[symmetric])
 qed
 
 interpretation eucl?: finite_dimensional_vector_space "scaleR :: real => 'a => 'a::euclidean_space" "Basis"
-  rewrites "module.dependent ( *\<^sub>R) = dependent"
-    and "module.representation ( *\<^sub>R) = representation"
-    and "module.subspace ( *\<^sub>R) = subspace"
-    and "module.span ( *\<^sub>R) = span"
-    and "vector_space.extend_basis ( *\<^sub>R) = extend_basis"
-    and "vector_space.dim ( *\<^sub>R) = dim"
-    and "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
-    and "Vector_Spaces.linear ( * ) ( *\<^sub>R) = linear"
+  rewrites "module.dependent (*\<^sub>R) = dependent"
+    and "module.representation (*\<^sub>R) = representation"
+    and "module.subspace (*\<^sub>R) = subspace"
+    and "module.span (*\<^sub>R) = span"
+    and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
+    and "vector_space.dim (*\<^sub>R) = dim"
+    and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
+    and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
     and "finite_dimensional_vector_space.dimension Basis = DIM('a)"
     and "dimension = DIM('a)"
   by (auto simp add: dependent_raw_def representation_raw_def
@@ -348,15 +348,15 @@
 
 interpretation eucl?: finite_dimensional_vector_space_prod scaleR scaleR Basis Basis
   rewrites "Basis_pair = Basis"
-    and "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
+    and "module_prod.scale (*\<^sub>R) (*\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
 proof -
-  show "finite_dimensional_vector_space_prod ( *\<^sub>R) ( *\<^sub>R) Basis Basis"
+  show "finite_dimensional_vector_space_prod (*\<^sub>R) (*\<^sub>R) Basis Basis"
     by unfold_locales
-  interpret finite_dimensional_vector_space_prod "( *\<^sub>R)" "( *\<^sub>R)" "Basis::'a set" "Basis::'b set"
+  interpret finite_dimensional_vector_space_prod "(*\<^sub>R)" "(*\<^sub>R)" "Basis::'a set" "Basis::'b set"
     by fact
   show "Basis_pair = Basis"
     unfolding Basis_pair_def Basis_prod_def by auto
-  show "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = scaleR"
+  show "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
     by (fact module_prod_scale_eq_scaleR)
 qed
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -235,7 +235,7 @@
 instantiation vec :: (times, finite) times
 begin
 
-definition "( * ) \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
+definition "(*) \<equiv> (\<lambda> x y.  (\<chi> i. (x$i) * (y$i)))"
 instance ..
 
 end
@@ -961,7 +961,7 @@
 lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)"
   by (simp add: vec_eq_iff)
 
-lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear ( * ) vector_scalar_mult vec"
+lemma Vector_Spaces_linear_vec [simp]: "Vector_Spaces.linear (*) vector_scalar_mult vec"
   by unfold_locales (vector algebra_simps)+
 
 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
@@ -1161,7 +1161,7 @@
 lemma%unimportant matrix_id_mat_1: "matrix id = mat 1"
   by (simp add: mat_def matrix_def axis_def)
 
-lemma%unimportant matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
+lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
   by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
 
 lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
@@ -1218,7 +1218,7 @@
 lemma%unimportant inj_matrix_vector_mult:
   fixes A::"'a::field^'n^'m"
   assumes "invertible A"
-  shows "inj (( *v) A)"
+  shows "inj ((*v) A)"
   by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
 
 lemma%important scalar_invertible:
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -929,7 +929,7 @@
       using E by (subst insert) (auto intro!: prod.cong)
     also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
        emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
-      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="( * )"] prod.cong)
+      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
     also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
       using insert(1,2) J E by (intro prod.mono_neutral_right) auto
     finally show "?\<mu> ?p = \<dots>" .
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -3549,12 +3549,12 @@
       by (intro conjI contg continuous_intros)
     show "(complex_of_real \<circ> g) ` S \<subseteq> \<real>"
       by auto
-    show "continuous_on \<real> (exp \<circ> ( * )\<i>)"
+    show "continuous_on \<real> (exp \<circ> (*)\<i>)"
       by (intro continuous_intros)
-    show "(exp \<circ> ( * )\<i>) ` \<real> \<subseteq> sphere 0 1"
+    show "(exp \<circ> (*)\<i>) ` \<real> \<subseteq> sphere 0 1"
       by (auto simp: complex_is_Real_iff)
   qed (auto simp: convex_Reals convex_imp_contractible)
-  moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> ( * )\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
+  moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> (*)\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
     by (simp add: g)
   ultimately show ?lhs
     apply (rule_tac x=a in exI)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -2049,7 +2049,7 @@
 
     moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
     hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
-      using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "( * )2" "2*z"]
+      using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "(*)2" "2*z"]
       by (intro tendsto_intros Gamma_series'_LIMSEQ)
          (simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
     ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
@@ -3131,10 +3131,10 @@
       case True
       have "(\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \<partial>lborel) = 
               (\<integral>\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1)) 
-                \<partial>distr lborel borel (( * ) (1 / u)))" (is "_ = nn_integral _ ?f")
+                \<partial>distr lborel borel ((*) (1 / u)))" (is "_ = nn_integral _ ?f")
         using True
         by (subst nn_integral_distr) (auto simp: indicator_def field_simps intro!: nn_integral_cong)
-      also have "distr lborel borel (( * ) (1 / u)) = density lborel (\<lambda>_. u)"
+      also have "distr lborel borel ((*) (1 / u)) = density lborel (\<lambda>_. u)"
         using \<open>u > 0\<close> by (subst lborel_distr_mult) auto
       also have "nn_integral \<dots> ?f = (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) *
                                               (u * (1 - x)) powr (b - 1))) \<partial>lborel)" using \<open>u > 0\<close>
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -225,7 +225,7 @@
     by (intro summable_Leibniz(1) decseq_imp_monoseq decseq_SucI) simp_all
   hence A: "(\<lambda>n. \<Sum>k<n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
     by (simp add: summable_sums_iff divide_inverse sums_def)
-  from filterlim_compose[OF this filterlim_subseq[of "( * ) (2::nat)"]]
+  from filterlim_compose[OF this filterlim_subseq[of "(*) (2::nat)"]]
     have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
     by (simp add: strict_mono_def)
   ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -5044,8 +5044,8 @@
       using real_arch_simple by blast
     have "ball 0 B \<subseteq> ?cube n" if n: "n \<ge> N" for n
     proof -
-      have "sum (( *\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
-            x \<bullet> i \<le> sum (( *\<^sub>R) (real n)) Basis \<bullet> i"
+      have "sum ((*\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
+            x \<bullet> i \<le> sum ((*\<^sub>R) (real n)) Basis \<bullet> i"
         if "norm x < B" "i \<in> Basis" for x i::'n
           using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf)
       then show ?thesis
@@ -5080,7 +5080,7 @@
         fix x :: 'n
         assume x: "x \<in> ball 0 B"
         have "\<lbrakk>norm (0 - x) < B; i \<in> Basis\<rbrakk>
-              \<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
+              \<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
           using Basis_le_norm[of i x] n by (auto simp add: field_simps sum_negf)
         then show "x \<in> ?cube n"
           using x by (auto simp: mem_box dist_norm)
@@ -6180,7 +6180,7 @@
     and bou: "bounded (range(\<lambda>k. integral S (f k)))"
   shows "g integrable_on S \<and> (\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
 proof -
-  have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = ( *\<^sub>R) (- 1) ` (range(\<lambda>k. integral S (f k)))"
+  have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = (*\<^sub>R) (- 1) ` (range(\<lambda>k. integral S (f k)))"
     by force
   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)"
   proof (rule monotone_convergence_increasing)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -835,9 +835,9 @@
   have "((sphere a r \<inter> T) - {b}) homeomorphic
         (+) (-a) ` ((sphere a r \<inter> T) - {b})"
     by (rule homeomorphic_translation)
-  also have "... homeomorphic ( *\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
+  also have "... homeomorphic (*\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
     by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
-  also have "... = sphere 0 1 \<inter> (( *\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
+  also have "... = sphere 0 1 \<inter> ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
     using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
   also have "... homeomorphic p"
     apply (rule homeomorphic_punctured_affine_sphere_affine_01)
@@ -2210,26 +2210,26 @@
                 and pq'_eq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p (q' t) = (f \<circ> g +++ reversepath g') t"
         using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] \<open>path q\<close> piq refl refl]
         by auto
-      have "q' t = (h \<circ> ( *\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
-      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])
-        show "q' 0 = (h \<circ> ( *\<^sub>R) 2) 0"
+      have "q' t = (h \<circ> (*\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
+      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])
+        show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
           by (metis \<open>pathstart q' = pathstart q\<close> comp_def g h pastq pathstart_def pth_4(2))
-        show "continuous_on {0..1/2} (f \<circ> g \<circ> ( *\<^sub>R) 2)"
+        show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
           apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
           using g(2) path_image_def by fastforce+
-        show "(f \<circ> g \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
+        show "(f \<circ> g \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
           using g(2) path_image_def fim by fastforce
-        show "(h \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
+        show "(h \<circ> (*\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
           using h path_image_def by fastforce
         show "q' ` {0..1/2} \<subseteq> C"
           using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
-        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p (q' x)"
+        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p (q' x)"
           by (auto simp: joinpaths_def pq'_eq)
-        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p ((h \<circ> ( *\<^sub>R) 2) x)"
+        show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> (*\<^sub>R) 2) x = p ((h \<circ> (*\<^sub>R) 2) x)"
           by (simp add: phg)
         show "continuous_on {0..1/2} q'"
           by (simp add: continuous_on_path \<open>path q'\<close>)
-        show "continuous_on {0..1/2} (h \<circ> ( *\<^sub>R) 2)"
+        show "continuous_on {0..1/2} (h \<circ> (*\<^sub>R) 2)"
           apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path h\<close>], force)
           done
       qed (use that in auto)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -277,7 +277,7 @@
 instantiation real :: real_inner
 begin
 
-definition inner_real_def [simp]: "inner = ( * )"
+definition inner_real_def [simp]: "inner = (*)"
 
 instance
 proof
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -767,10 +767,10 @@
   finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
 qed
 
-lemma lebesgue_measurable_scaling[measurable]: "( *\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+lemma lebesgue_measurable_scaling[measurable]: "(*\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
 proof cases
   assume "x = 0"
-  then have "( *\<^sub>R) x = (\<lambda>x. 0::'a)"
+  then have "(*\<^sub>R) x = (\<lambda>x. 0::'a)"
     by (auto simp: fun_eq_iff)
   then show ?thesis by auto
 next
@@ -860,9 +860,9 @@
 
 lemma lborel_distr_mult:
   assumes "(c::real) \<noteq> 0"
-  shows "distr lborel borel (( * ) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+  shows "distr lborel borel ((*) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
 proof-
-  have "distr lborel borel (( * ) c) = distr lborel lborel (( * ) c)" by (simp cong: distr_cong)
+  have "distr lborel borel ((*) c) = distr lborel lborel ((*) c)" by (simp cong: distr_cong)
   also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
     by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
   finally show ?thesis .
@@ -870,13 +870,13 @@
 
 lemma lborel_distr_mult':
   assumes "(c::real) \<noteq> 0"
-  shows "lborel = density (distr lborel borel (( * ) c)) (\<lambda>_. \<bar>c\<bar>)"
+  shows "lborel = density (distr lborel borel ((*) c)) (\<lambda>_. \<bar>c\<bar>)"
 proof-
   have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
   also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp
   also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)"
     by (subst density_density_eq) (auto simp: ennreal_mult)
-  also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (( * ) c)"
+  also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel ((*) c)"
     by (rule lborel_distr_mult[symmetric])
   finally show ?thesis .
 qed
@@ -1119,7 +1119,7 @@
 
   let ?f = "\<lambda>n. root DIM('a) (Suc n)"
 
-  have vimage_eq_image: "( *\<^sub>R) (?f n) -` S = ( *\<^sub>R) (1 / ?f n) ` S" for n
+  have vimage_eq_image: "(*\<^sub>R) (?f n) -` S = (*\<^sub>R) (1 / ?f n) ` S" for n
     apply safe
     subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
     subgoal by auto
@@ -1141,20 +1141,20 @@
     by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide)
   then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)"
     unfolding ennreal_suminf_multc eq by simp
-  also have "\<dots> = (\<Sum>n. emeasure lebesgue (( *\<^sub>R) (?f n) -` S))"
+  also have "\<dots> = (\<Sum>n. emeasure lebesgue ((*\<^sub>R) (?f n) -` S))"
     unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp
-  also have "\<dots> = emeasure lebesgue (\<Union>n. ( *\<^sub>R) (?f n) -` S)"
+  also have "\<dots> = emeasure lebesgue (\<Union>n. (*\<^sub>R) (?f n) -` S)"
   proof (intro suminf_emeasure)
-    show "disjoint_family (\<lambda>n. ( *\<^sub>R) (?f n) -` S)"
+    show "disjoint_family (\<lambda>n. (*\<^sub>R) (?f n) -` S)"
       unfolding disjoint_family_on_def
     proof safe
       fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S"
       with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}"
         by auto
     qed
-    have "( *\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
+    have "(*\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
       using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto
-    then show "range (\<lambda>i. ( *\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
+    then show "range (\<lambda>i. (*\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
       by auto
   qed
   also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -279,7 +279,7 @@
 lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="(+)"]
   and simple_function_diff[intro, simp] = simple_function_compose2[where h="(-)"]
   and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
-  and simple_function_mult[intro, simp] = simple_function_compose2[where h="( * )"]
+  and simple_function_mult[intro, simp] = simple_function_compose2[where h="(*)"]
   and simple_function_div[intro, simp] = simple_function_compose2[where h="(/)"]
   and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
   and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
@@ -760,7 +760,7 @@
     using assms by (intro simple_function_partition) auto
   also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ennreal))`space M.
     if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"
-    by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="( * )"] arg_cong2[where f=emeasure] sum.cong)
+    by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="(*)"] arg_cong2[where f=emeasure] sum.cong)
   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))"
     using assms by (subst sum.If_cases) (auto intro!: simple_functionD(1) simp: eq)
   also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ennreal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1737,7 +1737,7 @@
   show ?thesis
     unfolding path_component_def 
   proof (intro exI conjI)
-    have "continuous_on {0..1} (p \<circ> (( *) y))"
+    have "continuous_on {0..1} (p \<circ> ((*) y))"
       apply (rule continuous_intros)+
       using p [unfolded path_def] y
       apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Product_Vector.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -88,21 +88,21 @@
 
 end
 
-lemma module_prod_scale_eq_scaleR: "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = scaleR"
+lemma module_prod_scale_eq_scaleR: "module_prod.scale (*\<^sub>R) (*\<^sub>R) = scaleR"
   apply (rule ext) apply (rule ext)
   apply (subst module_prod.scale_def)
   subgoal by unfold_locales
   by (simp add: scaleR_prod_def)
 
 interpretation real_vector?: vector_space_prod "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
-  rewrites "scale = (( *\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
-    and "module.dependent ( *\<^sub>R) = dependent"
-    and "module.representation ( *\<^sub>R) = representation"
-    and "module.subspace ( *\<^sub>R) = subspace"
-    and "module.span ( *\<^sub>R) = span"
-    and "vector_space.extend_basis ( *\<^sub>R) = extend_basis"
-    and "vector_space.dim ( *\<^sub>R) = dim"
-    and "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
+  rewrites "scale = ((*\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
+    and "module.dependent (*\<^sub>R) = dependent"
+    and "module.representation (*\<^sub>R) = representation"
+    and "module.subspace (*\<^sub>R) = subspace"
+    and "module.span (*\<^sub>R) = span"
+    and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
+    and "vector_space.dim (*\<^sub>R) = dim"
+    and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
   subgoal by unfold_locales
   subgoal by (fact module_prod_scale_eq_scaleR)
   unfolding dependent_raw_def representation_raw_def subspace_raw_def span_raw_def
@@ -539,11 +539,11 @@
 proof -
   interpret p1: Vector_Spaces.linear s1 scale "(\<lambda>x. (x, 0))"
     by unfold_locales (auto simp: scale_def)
-  interpret pair1: finite_dimensional_vector_space_pair "( *a)" B1 scale Basis_pair
+  interpret pair1: finite_dimensional_vector_space_pair "(*a)" B1 scale Basis_pair
     by unfold_locales
   interpret p2: Vector_Spaces.linear s2 scale "(\<lambda>x. (0, x))"
     by unfold_locales (auto simp: scale_def)
-  interpret pair2: finite_dimensional_vector_space_pair "( *b)" B2 scale Basis_pair
+  interpret pair2: finite_dimensional_vector_space_pair "(*b)" B2 scale Basis_pair
     by unfold_locales
   have ss: "p.subspace ((\<lambda>x. (x, 0)) ` S)" "p.subspace (Pair 0 ` T)"
     by (rule p1.subspace_image p2.subspace_image assms)+
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -138,17 +138,17 @@
     proof (intro bdd_aboveI exI ballI, clarify)
       show "norm (deriv f 0) \<le> 1 / r" if "f \<in> F" for f
       proof -
-        have r01: "( * ) (complex_of_real r) ` ball 0 1 \<subseteq> S"
+        have r01: "(*) (complex_of_real r) ` ball 0 1 \<subseteq> S"
           using that \<open>r > 0\<close> by (auto simp: norm_mult r [THEN subsetD])
-        then have "f holomorphic_on ( * ) (complex_of_real r) ` ball 0 1"
+        then have "f holomorphic_on (*) (complex_of_real r) ` ball 0 1"
           using holomorphic_on_subset [OF holF] by (simp add: that)
         then have holf: "f \<circ> (\<lambda>z. (r * z)) holomorphic_on (ball 0 1)"
           by (intro holomorphic_intros holomorphic_on_compose)
-        have f0: "(f \<circ> ( * ) (complex_of_real r)) 0 = 0"
+        have f0: "(f \<circ> (*) (complex_of_real r)) 0 = 0"
           using F_def that by auto
         have "f ` S \<subseteq> ball 0 1"
           using F_def that by blast
-        with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> ( * )(of_real r))z) < 1"
+        with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> (*)(of_real r))z) < 1"
           by force
         have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
           if "z \<in> ball 0 1" for z::complex
@@ -162,7 +162,7 @@
           using * [of 0] by simp
         have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
           using DERIV_imp_deriv df0 by blast
-        have "norm (deriv (f \<circ> ( * ) (complex_of_real r)) 0) \<le> 1"
+        have "norm (deriv (f \<circ> (*) (complex_of_real r)) 0) \<le> 1"
           by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
         with \<open>r > 0\<close> show ?thesis
           by (simp add: deq norm_mult divide_simps o_def)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -2902,22 +2902,22 @@
 lemma rel_interior_scaleR:
   fixes S :: "'n::euclidean_space set"
   assumes "c \<noteq> 0"
-  shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
-  using rel_interior_injective_linear_image[of "(( *\<^sub>R) c)" S]
-    linear_conv_bounded_linear[of "( *\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
+  shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
+  using rel_interior_injective_linear_image[of "((*\<^sub>R) c)" S]
+    linear_conv_bounded_linear[of "(*\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
   by auto
 
 lemma rel_interior_convex_scaleR:
   fixes S :: "'n::euclidean_space set"
   assumes "convex S"
-  shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
+  shows "((*\<^sub>R) c) ` (rel_interior S) = rel_interior (((*\<^sub>R) c) ` S)"
   by (metis assms linear_scaleR rel_interior_convex_linear_image)
 
 lemma convex_rel_open_scaleR:
   fixes S :: "'n::euclidean_space set"
   assumes "convex S"
     and "rel_open S"
-  shows "convex ((( *\<^sub>R) c) ` S) \<and> rel_open ((( *\<^sub>R) c) ` S)"
+  shows "convex (((*\<^sub>R) c) ` S) \<and> rel_open (((*\<^sub>R) c) ` S)"
   by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
 
 lemma convex_rel_open_finite_inter:
@@ -3086,10 +3086,10 @@
     by (simp add: rel_interior_empty cone_0)
 next
   case False
-  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
+  then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
     using cone_iff[of S] assms by auto
   then have *: "0 \<in> ({0} \<union> rel_interior S)"
-    and "\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
+    and "\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
     by (auto simp add: rel_interior_scaleR)
   then show ?thesis
     using cone_iff[of "{0} \<union> rel_interior S"] by auto
@@ -3099,7 +3099,7 @@
   fixes S :: "'m::euclidean_space set"
   assumes "convex S"
   shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow>
-    c > 0 \<and> x \<in> ((( *\<^sub>R) c) ` (rel_interior S))"
+    c > 0 \<and> x \<in> (((*\<^sub>R) c) ` (rel_interior S))"
 proof (cases "S = {}")
   case True
   then show ?thesis
@@ -3132,9 +3132,9 @@
   {
     fix c :: real
     assume "c > 0"
-    then have "f c = (( *\<^sub>R) c ` S)"
+    then have "f c = ((*\<^sub>R) c ` S)"
       using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
-    then have "rel_interior (f c) = ( *\<^sub>R) c ` rel_interior S"
+    then have "rel_interior (f c) = (*\<^sub>R) c ` rel_interior S"
       using rel_interior_convex_scaleR[of S c] assms by auto
   }
   then show ?thesis using * ** by auto
@@ -8025,7 +8025,7 @@
         by auto
       have "b \<bullet> (v - ?u) = 0" if "b \<in> B" for b
         using that \<open>finite B\<close>
-        by (simp add: * algebra_simps inner_sum_right if_distrib [of "( *)v" for v] inner_commute cong: if_cong)
+        by (simp add: * algebra_simps inner_sum_right if_distrib [of "(*)v" for v] inner_commute cong: if_cong)
       then show "y \<bullet> (v - ?u) = 0"
         by (simp add: u inner_sum_left)
     qed
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Analysis/normarith.ML
--- a/src/HOL/Analysis/normarith.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Analysis/normarith.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -26,7 +26,7 @@
  fun find_normedterms t acc = case Thm.term_of t of
     @{term "(+) :: real => _"}$_$_ =>
             find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
-      | @{term "( * ) :: real => _"}$_$_ =>
+      | @{term "(*) :: real => _"}$_$_ =>
             if not (is_ratconst (Thm.dest_arg1 t)) then acc else
             augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0)
                       (Thm.dest_arg t) acc
@@ -83,7 +83,7 @@
 
 fun replacenegnorms cv t = case Thm.term_of t of
   @{term "(+) :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
-| @{term "( * ) :: real => _"}$_$_ =>
+| @{term "(*) :: real => _"}$_$_ =>
     if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
 | _ => Thm.reflexive t
 (*
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Binomial.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1299,7 +1299,7 @@
   "n choose k =
       (if k > n then 0
        else if 2 * k > n then n choose (n - k)
-       else (fold_atLeastAtMost_nat ( * ) (n - k + 1) n 1 div fact k))"
+       else (fold_atLeastAtMost_nat (*) (n - k + 1) n 1 div fact k))"
 proof -
   {
     assume "k \<le> n"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -421,7 +421,7 @@
     Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
     Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd ( * ) = Rings.dvd"
+    rewrites "dvd.dvd (*) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
   proof (rule ext)+
@@ -575,7 +575,7 @@
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd ( * ) = Rings.dvd"
+    rewrites "dvd.dvd (*) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
   proof (rule ext)+
@@ -612,7 +612,7 @@
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd ( * ) = Rings.dvd"
+    rewrites "dvd.dvd (*) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
   proof (rule ext)+
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -78,7 +78,7 @@
 
 instantiation fps :: ("{comm_monoid_add, times}") times
 begin
-  definition fps_times_def: "( * ) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
+  definition fps_times_def: "(*) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))"
   instance ..
 end
 
@@ -2037,7 +2037,7 @@
   (* If f reprents {a_n} and P is a polynomial, then
         P(xD) f represents {P(n) a_n}*)
 
-definition "fps_XD = ( * ) fps_X \<circ> fps_deriv"
+definition "fps_XD = (*) fps_X \<circ> fps_deriv"
 
 lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)"
   by (simp add: fps_XD_def field_simps)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -891,7 +891,7 @@
 lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
   by (induct n) (simp_all add: monom_0 monom_Suc)
 
-lemma smult_Poly: "smult c (Poly xs) = Poly (map (( * ) c) xs)"
+lemma smult_Poly: "smult c (Poly xs) = Poly (map ((*) c) xs)"
   by (auto simp: poly_eq_iff nth_default_def)
 
 lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)"
@@ -3811,10 +3811,10 @@
   where
     "pseudo_divmod_main_list lc q r d (Suc n) =
       (let
-        rr = map (( * ) lc) r;
+        rr = map ((*) lc) r;
         a = hd r;
-        qqq = cCons a (map (( * ) lc) q);
-        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (( * ) a) d))
+        qqq = cCons a (map ((*) lc) q);
+        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d))
        in pseudo_divmod_main_list lc qqq rrr d n)"
   | "pseudo_divmod_main_list lc q r d 0 = (q, r)"
 
@@ -3822,9 +3822,9 @@
   where
     "pseudo_mod_main_list lc r d (Suc n) =
       (let
-        rr = map (( * ) lc) r;
+        rr = map ((*) lc) r;
         a = hd r;
-        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map (( * ) a) d))
+        rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d))
        in pseudo_mod_main_list lc rrr d n)"
   | "pseudo_mod_main_list lc r d 0 = r"
 
@@ -3836,7 +3836,7 @@
       (let
         a = hd r;
         qqq = cCons a q;
-        rr = tl (if a = 0 then r else minus_poly_rev_list r (map (( * ) a) d))
+        rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d))
        in divmod_poly_one_main_list qqq rr d n)"
   | "divmod_poly_one_main_list q r d 0 = (q, r)"
 
@@ -3845,7 +3845,7 @@
     "mod_poly_one_main_list r d (Suc n) =
       (let
         a = hd r;
-        rr = tl (if a = 0 then r else minus_poly_rev_list r (map (( * ) a) d))
+        rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d))
        in mod_poly_one_main_list rr d n)"
   | "mod_poly_one_main_list r d 0 = r"
 
@@ -3866,7 +3866,7 @@
         re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q)
        in rev re))"
 
-lemma minus_zero_does_nothing: "minus_poly_rev_list x (map (( * ) 0) y) = x"
+lemma minus_zero_does_nothing: "minus_poly_rev_list x (map ((*) 0) y) = x"
   for x :: "'a::ring list"
   by (induct x y rule: minus_poly_rev_list.induct) auto
 
@@ -3874,8 +3874,8 @@
   by (induct xs ys rule: minus_poly_rev_list.induct) auto
 
 lemma if_0_minus_poly_rev_list:
-  "(if a = 0 then x else minus_poly_rev_list x (map (( * ) a) y)) =
-    minus_poly_rev_list x (map (( * ) a) y)"
+  "(if a = 0 then x else minus_poly_rev_list x (map ((*) a) y)) =
+    minus_poly_rev_list x (map ((*) a) y)"
   for a :: "'a::ring"
   by(cases "a = 0") (simp_all add: minus_zero_does_nothing)
 
@@ -3917,7 +3917,7 @@
 
 lemma head_minus_poly_rev_list:
   "length d \<le> length r \<Longrightarrow> d \<noteq> [] \<Longrightarrow>
-    hd (minus_poly_rev_list (map (( * ) (last d)) r) (map (( * ) (hd r)) (rev d))) = 0"
+    hd (minus_poly_rev_list (map ((*) (last d)) r) (map ((*) (hd r)) (rev d))) = 0"
   for d r :: "'a::comm_ring list"
 proof (induct r)
   case Nil
@@ -3927,7 +3927,7 @@
   then show ?case by (cases "rev d") (simp_all add: ac_simps)
 qed
 
-lemma Poly_map: "Poly (map (( * ) a) p) = smult a (Poly p)"
+lemma Poly_map: "Poly (map ((*) a) p) = smult a (Poly p)"
 proof (induct p)
   case Nil
   then show ?case by simp
@@ -3955,9 +3955,9 @@
   with \<open>d \<noteq> []\<close> have "r \<noteq> []"
     using Suc_leI length_greater_0_conv list.size(3) by fastforce
   let ?a = "(hd (rev r))"
-  let ?rr = "map (( * ) lc) (rev r)"
-  let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map (( * ) ?a) (rev d))))"
-  let ?qq = "cCons ?a (map (( * ) lc) q)"
+  let ?rr = "map ((*) lc) (rev r)"
+  let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map ((*) ?a) (rev d))))"
+  let ?qq = "cCons ?a (map ((*) lc) q)"
   from * Suc(3) have n: "n = (1 + length r - length d - 1)"
     by simp
   from * have rr_val:"(length ?rrr) = (length r - 1)"
@@ -3990,12 +3990,12 @@
     case 2
     show ?case
     proof (subst Poly_on_rev_starting_with_0, goal_cases)
-      show "hd (minus_poly_rev_list (map (( * ) lc) (rev r)) (map (( * ) (hd (rev r))) (rev d))) = 0"
+      show "hd (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))) = 0"
         by (fold lc, subst head_minus_poly_rev_list, insert * \<open>d \<noteq> []\<close>, auto)
       from * have "length d \<le> length r"
         by simp
       then show "smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d =
-          Poly (rev (minus_poly_rev_list (map (( * ) lc) (rev r)) (map (( * ) (hd (rev r))) (rev d))))"
+          Poly (rev (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))))"
         by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
             minus_poly_rev_list)
     qed
@@ -4100,9 +4100,9 @@
         let
           cf = coeffs f;
           ilc = inverse (last cg);
-          ch = map (( * ) ilc) cg;
+          ch = map ((*) ilc) cg;
           (q, r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg)
-        in (poly_of_list (map (( * ) ilc) q), poly_of_list (rev r)))"
+        in (poly_of_list (map ((*) ilc) q), poly_of_list (rev r)))"
 proof -
   note d = pdivmod_via_pseudo_divmod pseudo_divmod_impl pseudo_divmod_list_def
   show ?thesis
@@ -4121,10 +4121,10 @@
     have id2: "hd (rev (coeffs (smult ilc g))) = 1"
       by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def)
     have id3: "length (coeffs (smult ilc g)) = length (coeffs g)"
-      "rev (coeffs (smult ilc g)) = rev (map (( * ) ilc) (coeffs g))"
+      "rev (coeffs (smult ilc g)) = rev (map ((*) ilc) (coeffs g))"
       unfolding coeffs_smult using ilc by auto
     obtain q r where pair:
-      "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map (( * ) ilc) (coeffs g)))
+      "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map ((*) ilc) (coeffs g)))
         (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
       by force
     show ?thesis
@@ -4137,7 +4137,7 @@
 lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list"
 proof (intro ext, goal_cases)
   case (1 q r d n)
-  have *: "map (( * ) 1) xs = xs" for xs :: "'a list"
+  have *: "map ((*) 1) xs = xs" for xs :: "'a list"
     by (induct xs) auto
   show ?case
     by (induct n arbitrary: q r d) (auto simp: * Let_def)
@@ -4151,7 +4151,7 @@
         in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let
         a = cr div lc;
         qq = cCons a q;
-        rr = minus_poly_rev_list r (map (( * ) a) d)
+        rr = minus_poly_rev_list r (map ((*) a) d)
        in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
   | "divide_poly_main_list lc q r d 0 = q"
 
@@ -4161,7 +4161,7 @@
       cr = hd r;
       a = cr div lc;
       qq = cCons a q;
-      rr = minus_poly_rev_list r (map (( * ) a) d)
+      rr = minus_poly_rev_list r (map ((*) a) d)
      in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
   by (simp add: Let_def minus_zero_does_nothing)
 
@@ -4190,7 +4190,7 @@
         let
           cf = coeffs f;
           ilc = inverse (last cg);
-          ch = map (( * ) ilc) cg;
+          ch = map ((*) ilc) cg;
           r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg)
         in poly_of_list (rev r))"
   (is "_ = ?rhs")
@@ -4209,9 +4209,9 @@
         let
           cf = coeffs f;
           ilc = inverse (last cg);
-          ch = map (( * ) ilc) cg;
+          ch = map ((*) ilc) cg;
           q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg))
-        in poly_of_list ((map (( * ) ilc) q)))"
+        in poly_of_list ((map ((*) ilc) q)))"
 
 text \<open>We do not declare the following lemma as code equation, since then polynomial division
   on non-fields will no longer be executable. However, a code-unfold is possible, since
@@ -4259,7 +4259,7 @@
     with r d have id:
       "?thesis \<longleftrightarrow>
         Poly (divide_poly_main_list lc (cCons (lcr div lc) q)
-          (rev (rev (minus_poly_rev_list (rev rr) (rev (map (( * ) (lcr div lc)) dd))))) (rev d) n) =
+          (rev (rev (minus_poly_rev_list (rev rr) (rev (map ((*) (lcr div lc)) dd))))) (rev d) n) =
           divide_poly_main lc
             (monom 1 (Suc n) * Poly q + monom (lcr div lc) n)
             (Poly r - monom (lcr div lc) n * Poly d)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Decision_Procs/Algebra_Aux.thy
--- a/src/HOL/Decision_Procs/Algebra_Aux.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Algebra_Aux.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -234,7 +234,7 @@
   by (induct n) (simp_all add: m_ac)
 
 definition cring_class_ops :: "'a::comm_ring_1 ring"
-  where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
+  where "cring_class_ops \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>"
 
 lemma cring_class: "cring cring_class_ops"
   apply unfold_locales
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -2402,7 +2402,7 @@
       @{code Add} (num_of_term vs t1, num_of_term vs t2)
   | num_of_term vs (@{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (@{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+  | num_of_term vs (@{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
       (case try HOLogic.dest_number t1 of
         SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
       | NONE =>
@@ -2455,7 +2455,7 @@
       term_of_num vs t1 $ term_of_num vs t2
   | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} $
       term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} $
+  | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: int \<Rightarrow> int \<Rightarrow> int"} $
       term_of_num vs (@{code C} i) $ term_of_num vs t2
   | term_of_num vs (@{code CN} (n, i, t)) =
       term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -2476,7 +2476,7 @@
      @{code Add} (num_of_term vs t1, num_of_term vs t2)
   | num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
      @{code Sub} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (@{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
+  | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) = (case num_of_term vs t1
      of @{code C} i => @{code Mul} (i, num_of_term vs t2)
       | _ => error "num_of_term: unsupported multiplication")
   | num_of_term vs (@{term "real_of_int :: int \<Rightarrow> real"} $ t') =
@@ -2514,7 +2514,7 @@
       term_of_num vs t1 $ term_of_num vs t2
   | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $
       term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $
+  | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $
       term_of_num vs (@{code C} i) $ term_of_num vs t2
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -5579,7 +5579,7 @@
       @{code Add} (num_of_term vs t1, num_of_term vs t2)
   | num_of_term vs (@{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
-  | num_of_term vs (@{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
+  | num_of_term vs (@{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $ t1 $ t2) =
       (case (num_of_term vs t1)
        of @{code C} i => @{code Mul} (i, num_of_term vs t2)
         | _ => error "num_of_term: unsupported Multiplication")
@@ -5638,7 +5638,7 @@
       term_of_num vs t1 $ term_of_num vs t2
   | term_of_num vs (@{code Sub} (t1, t2)) = @{term "(-) :: real \<Rightarrow> real \<Rightarrow> real"} $
       term_of_num vs t1 $ term_of_num vs t2
-  | term_of_num vs (@{code Mul} (i, t2)) = @{term "( * ) :: real \<Rightarrow> real \<Rightarrow> real"} $
+  | term_of_num vs (@{code Mul} (i, t2)) = @{term "(*) :: real \<Rightarrow> real \<Rightarrow> real"} $
       term_of_num vs (@{code C} i) $ term_of_num vs t2
   | term_of_num vs (@{code Floor} t) = @{term "of_int :: int \<Rightarrow> real"} $ (@{term "floor :: real \<Rightarrow> int"} $ term_of_num vs t)
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -186,7 +186,7 @@
     by (cases "x = zero") (auto simp add: distrib_left ac_simps)
 qed
 
-lemma (in comm_semiring_0) poly_cmult_map: "poly (map (( * ) c) p) x = c * poly p x"
+lemma (in comm_semiring_0) poly_cmult_map: "poly (map ((*) c) p) x = c * poly p x"
   by (induct p) (auto simp add: distrib_left ac_simps)
 
 lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Deriv.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -38,7 +38,7 @@
 
 definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
     (infix "(has'_field'_derivative)" 50)
-  where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative ( * ) D) F"
+  where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative (*) D) F"
 
 lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
   by simp
@@ -153,7 +153,7 @@
 
 lemma field_has_derivative_at:
   fixes x :: "'a::real_normed_field"
-  shows "(f has_derivative ( * ) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
+  shows "(f has_derivative (*) D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D" (is "?lhs = ?rhs")
 proof -
   have "?lhs = (\<lambda>h. norm (f (x + h) - f x - D * h) / norm h) \<midarrow>0 \<rightarrow> 0"
     by (simp add: bounded_linear_mult_right has_derivative_at)
@@ -648,7 +648,7 @@
   by (rule has_derivative_eq_rhs[of f D]) (simp_all add: fun_eq_iff mult.commute)
 
 lemma has_field_derivative_imp_has_derivative:
-  "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative ( * ) D) F"
+  "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative (*) D) F"
   by (simp add: has_field_derivative_def)
 
 lemma DERIV_subset:
@@ -675,7 +675,7 @@
   assume "f differentiable at x within s"
   then obtain f' where *: "(f has_derivative f') (at x within s)"
     unfolding differentiable_def by auto
-  then obtain c where "f' = (( * ) c)"
+  then obtain c where "f' = ((*) c)"
     by (metis real_bounded_linear has_derivative_bounded_linear mult.commute fun_eq_iff)
   with * show "\<exists>D. (f has_real_derivative D) (at x within s)"
     unfolding has_field_derivative_def by auto
@@ -702,7 +702,7 @@
 lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
 
-lemma mult_commute_abs: "(\<lambda>x. x * c) = ( * ) c"
+lemma mult_commute_abs: "(\<lambda>x. x * c) = (*) c"
   for c :: "'a::ab_semigroup_mult"
   by (simp add: fun_eq_iff mult.commute)
 
@@ -711,7 +711,7 @@
   assumes "DERIV f (g x) :> f'"
   assumes "(g has_derivative g') (at x within s)"
   shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
-  using assms has_derivative_compose[of g g' x s f "( * ) f'"]
+  using assms has_derivative_compose[of g g' x s f "(*) f'"]
   by (auto simp: has_field_derivative_def ac_simps)
 
 
@@ -896,7 +896,7 @@
     ((\<lambda>x. f x * c) has_field_derivative D * c) (at x within s)"
   using DERIV_cmult by (auto simp add: ac_simps)
 
-lemma DERIV_cmult_Id [simp]: "(( * ) c has_field_derivative c) (at x within s)"
+lemma DERIV_cmult_Id [simp]: "((*) c has_field_derivative c) (at x within s)"
   using DERIV_ident [THEN DERIV_cmult, where c = c and x = x] by simp
 
 lemma DERIV_cdivide:
@@ -919,7 +919,7 @@
   shows "((\<lambda>x. inverse (f x)) has_field_derivative - (inverse (f x) * D * inverse (f x)))
     (at x within s)"
 proof -
-  have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative ( * ) D)"
+  have "(f has_derivative (\<lambda>x. x * D)) = (f has_derivative (*) D)"
     by (rule arg_cong [of "\<lambda>x. x * D"]) (simp add: fun_eq_iff)
   with assms have "(f has_derivative (\<lambda>x. x * D)) (at x within s)"
     by (auto dest!: has_field_derivative_imp_has_derivative)
@@ -972,7 +972,7 @@
 
 lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow>
   ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
-  using has_derivative_compose[of f "( * ) D" x s g "( * ) E"]
+  using has_derivative_compose[of f "(*) D" x s g "(*) E"]
   by (simp only: has_field_derivative_def mult_commute_abs ac_simps)
 
 corollary DERIV_chain2: "DERIV f (g x) :> Da \<Longrightarrow> (g has_field_derivative Db) (at x within s) \<Longrightarrow>
@@ -990,7 +990,7 @@
   "(f has_field_derivative Da) (at (g x) within (g ` s)) \<Longrightarrow>
     (g has_field_derivative Db) (at x within s) \<Longrightarrow>
     (f \<circ> g has_field_derivative Da * Db) (at x within s)"
-  using has_derivative_in_compose [of g "( * ) Db" x s f "( * ) Da "]
+  using has_derivative_in_compose [of g "(*) Db" x s f "(*) Da "]
   by (simp add: has_field_derivative_def o_def mult_commute_abs ac_simps)
 
 (*These two are from HOL Light: HAS_COMPLEX_DERIVATIVE_CHAIN*)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Enum.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -585,7 +585,7 @@
 definition [simp]: "Groups.zero = a\<^sub>1"
 definition [simp]: "Groups.one = a\<^sub>1"
 definition [simp]: "(+) = (\<lambda>_ _. a\<^sub>1)"
-definition [simp]: "( * ) = (\<lambda>_ _. a\<^sub>1)"
+definition [simp]: "(*) = (\<lambda>_ _. a\<^sub>1)"
 definition [simp]: "(mod) = (\<lambda>_ _. a\<^sub>1)" 
 definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
 definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
@@ -690,7 +690,7 @@
 definition "(-) = ((+) :: finite_2 \<Rightarrow> _)"
 definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
 definition "inverse = (\<lambda>x :: finite_2. x)"
-definition "divide = (( * ) :: finite_2 \<Rightarrow> _)"
+definition "divide = ((*) :: finite_2 \<Rightarrow> _)"
 definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
 definition "abs = (\<lambda>x :: finite_2. x)"
 definition "sgn = (\<lambda>x :: finite_2. x)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Factorial.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -403,13 +403,13 @@
 subsection \<open>Misc\<close>
 
 lemma fact_code [code]:
-  "fact n = (of_nat (fold_atLeastAtMost_nat (( * )) 2 n 1) :: 'a::semiring_char_0)"
+  "fact n = (of_nat (fold_atLeastAtMost_nat ((*)) 2 n 1) :: 'a::semiring_char_0)"
 proof -
   have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
     by (simp add: fact_prod)
   also have "\<Prod>{1..n} = \<Prod>{2..n}"
     by (intro prod.mono_neutral_right) auto
-  also have "\<dots> = fold_atLeastAtMost_nat (( * )) 2 n 1"
+  also have "\<dots> = fold_atLeastAtMost_nat ((*)) 2 n 1"
     by (simp add: prod_atLeastAtMost_code)
   finally show ?thesis .
 qed
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/GCD.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -976,25 +976,25 @@
 lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
   by (blast dest: dvd_GcdD intro: Gcd_greatest)
 
-lemma Gcd_mult: "Gcd (( *) c ` A) = normalize c * Gcd A"
+lemma Gcd_mult: "Gcd ((*) c ` A) = normalize c * Gcd A"
 proof (cases "c = 0")
   case True
   then show ?thesis by auto
 next
   case [simp]: False
-  have "Gcd (( *) c ` A) div c dvd Gcd A"
+  have "Gcd ((*) c ` A) div c dvd Gcd A"
     by (intro Gcd_greatest, subst div_dvd_iff_mult)
        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
-  then have "Gcd (( *) c ` A) dvd c * Gcd A"
+  then have "Gcd ((*) c ` A) dvd c * Gcd A"
     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
   also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
-  also have "Gcd (( *) c ` A) dvd \<dots> \<longleftrightarrow> Gcd (( *) c ` A) dvd normalize c * Gcd A"
+  also have "Gcd ((*) c ` A) dvd \<dots> \<longleftrightarrow> Gcd ((*) c ` A) dvd normalize c * Gcd A"
     by (simp add: dvd_mult_unit_iff)
-  finally have "Gcd (( *) c ` A) dvd normalize c * Gcd A" .
-  moreover have "normalize c * Gcd A dvd Gcd (( *) c ` A)"
+  finally have "Gcd ((*) c ` A) dvd normalize c * Gcd A" .
+  moreover have "normalize c * Gcd A dvd Gcd ((*) c ` A)"
     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
-  ultimately have "normalize (Gcd (( *) c ` A)) = normalize (normalize c * Gcd A)"
+  ultimately have "normalize (Gcd ((*) c ` A)) = normalize (normalize c * Gcd A)"
     by (rule associatedI)
   then show ?thesis
     by (simp add: normalize_mult)
@@ -1015,10 +1015,10 @@
 
 lemma Lcm_mult:
   assumes "A \<noteq> {}"
-  shows "Lcm (( *) c ` A) = normalize c * Lcm A"
+  shows "Lcm ((*) c ` A) = normalize c * Lcm A"
 proof (cases "c = 0")
   case True
-  with assms have "( *) c ` A = {0}"
+  with assms have "(*) c ` A = {0}"
     by auto
   with True show ?thesis by auto
 next
@@ -1027,23 +1027,23 @@
     by blast
   have "c dvd c * x"
     by simp
-  also from x have "c * x dvd Lcm (( *) c ` A)"
+  also from x have "c * x dvd Lcm ((*) c ` A)"
     by (intro dvd_Lcm) auto
-  finally have dvd: "c dvd Lcm (( *) c ` A)" .
-
-  have "Lcm A dvd Lcm (( *) c ` A) div c"
+  finally have dvd: "c dvd Lcm ((*) c ` A)" .
+
+  have "Lcm A dvd Lcm ((*) c ` A) div c"
     by (intro Lcm_least dvd_mult_imp_div)
       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
-  then have "c * Lcm A dvd Lcm (( *) c ` A)"
+  then have "c * Lcm A dvd Lcm ((*) c ` A)"
     by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
-  also have "\<dots> dvd Lcm (( *) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (( *) c ` A)"
+  also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
     by (simp add: mult_unit_dvd_iff)
-  finally have "normalize c * Lcm A dvd Lcm (( *) c ` A)" .
-  moreover have "Lcm (( *) c ` A) dvd normalize c * Lcm A"
+  finally have "normalize c * Lcm A dvd Lcm ((*) c ` A)" .
+  moreover have "Lcm ((*) c ` A) dvd normalize c * Lcm A"
     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
-  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (( *) c ` A))"
+  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm ((*) c ` A))"
     by (rule associatedI)
   then show ?thesis
     by (simp add: normalize_mult)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Groups_List.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -124,7 +124,7 @@
   by (induct xss) simp_all
 
 lemma (in monoid_add) length_product_lists:
-  "length (product_lists xss) = foldr ( * ) (map length xss) 1"
+  "length (product_lists xss) = foldr (*) (map length xss) 1"
 proof (induct xss)
   case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
 qed simp
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -60,7 +60,7 @@
     and (OCaml) "Pervasives.( +. )"
 
 code_printing
-  constant "( * ) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+  constant "(*) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
     (SML) "Real.* ((_), (_))"
     and (OCaml) "Pervasives.( *. )"
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -372,7 +372,7 @@
 
 end
 
-\<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>
+\<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>
 lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((+) a) ^^ n)) 0 ms"
   unfolding sum_mset.eq_fold
   apply (rule comp_fun_commute.DAList_Multiset_fold)
@@ -380,8 +380,8 @@
   apply (auto simp: ac_simps)
   done
 
-\<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>
-lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((( * ) a) ^^ n)) 1 ms"
+\<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>
+lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((*) a) ^^ n)) 1 ms"
   unfolding prod_mset.eq_fold
   apply (rule comp_fun_commute.DAList_Multiset_fold)
   apply unfold_locales
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Discrete.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -274,7 +274,7 @@
       then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})"
         using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute)
       then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps)
-      moreover have "finite (( * ) q ` {m. m * m \<le> n})"
+      moreover have "finite ((*) q ` {m. m * m \<le> n})"
         by (metis (mono_tags) finite_imageI finite_less_ub le_square)
       moreover have "\<exists>x. x * x \<le> n"
         by (metis \<open>q * q \<le> n\<close>)
@@ -282,7 +282,7 @@
         by simp (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans)
     qed
   qed
-  then have "Max (( * ) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
+  then have "Max ((*) (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n"
     apply (subst Max_le_iff)
       apply (metis (mono_tags) finite_imageI finite_less_ub le_square)
      apply auto
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -262,7 +262,7 @@
 lift_definition one_ennreal :: ennreal is 1 by simp
 lift_definition zero_ennreal :: ennreal is 0 by simp
 lift_definition plus_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(+)" by simp
-lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "( * )" by simp
+lift_definition times_ennreal :: "ennreal \<Rightarrow> ennreal \<Rightarrow> ennreal" is "(*)" by simp
 
 instance
   by standard (transfer; auto simp: field_simps ereal_right_distrib)+
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Float.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -202,7 +202,7 @@
 lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(+)" by simp
 declare plus_float.rep_eq[simp]
 
-lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "( * )" by simp
+lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(*)" by simp
 declare times_float.rep_eq[simp]
 
 lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(-)" by simp
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/ListVector.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -13,7 +13,7 @@
 text\<open>Multiplication with a scalar:\<close>
 
 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
-where "x *\<^sub>s xs \<equiv> map (( * ) x) xs"
+where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
 
 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
 by (induct xs) simp_all
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -221,7 +221,7 @@
   val neg_tm = \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
   val add_tm = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
   val sub_tm = \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
-  val mul_tm = \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close>
+  val mul_tm = \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
   val inv_tm = \<^cterm>\<open>inverse :: real \<Rightarrow> _\<close>
   val div_tm = \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
   val pow_tm = \<^cterm>\<open>(^) :: real \<Rightarrow> _\<close>
@@ -862,7 +862,7 @@
       Free (_, \<^typ>\<open>real\<close>) =>
         if not (member (op aconvc) fvs tm) then (@1, tm)
         else raise Failure "substitutable_monomial"
-    | \<^term>\<open>( * ) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
+    | \<^term>\<open>(*) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
         if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
           not (member (op aconvc) fvs (Thm.dest_arg tm))
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
@@ -899,7 +899,7 @@
         val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
         val th1 =
           Drule.arg_cong_rule
-            (Thm.apply \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
+            (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
             (mk_meta_eq th)
         val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1
       in fconv_rule (arg_conv (real_poly_conv ctxt)) (isolate_variable v th2) end
@@ -943,7 +943,7 @@
    \<^term>\<open>(=) :: real \<Rightarrow> _\<close>, \<^term>\<open>(<) :: real \<Rightarrow> _\<close>,
    \<^term>\<open>(\<le>) :: real \<Rightarrow> _\<close>,
    \<^term>\<open>(+) :: real \<Rightarrow> _\<close>, \<^term>\<open>(-) :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>( * ) :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
+   \<^term>\<open>(*) :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
    \<^term>\<open>(/) :: real \<Rightarrow> _\<close>, \<^term>\<open>inverse :: real \<Rightarrow> _\<close>,
    \<^term>\<open>(^) :: real \<Rightarrow> _\<close>, \<^term>\<open>abs :: real \<Rightarrow> _\<close>,
    \<^term>\<open>min :: real \<Rightarrow> _\<close>, \<^term>\<open>max :: real \<Rightarrow> _\<close>,
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -328,13 +328,13 @@
     let
       val m' = FuncUtil.dest_monomial m
       val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
-    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close> s) t) vps
+    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> s) t) vps
     end
 
 fun cterm_of_cmonomial (m,c) =
   if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   else if c = @1 then cterm_of_monomial m
-  else Thm.apply (Thm.apply \<^cterm>\<open>( * )::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
+  else Thm.apply (Thm.apply \<^cterm>\<open>(*)::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
 
 fun cterm_of_poly p =
   if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\<open>0::real\<close>
@@ -680,7 +680,7 @@
           in
             if opr aconvc \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
             then linear_add (lin_of_hol l) (lin_of_hol r)
-            else if opr aconvc \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close>
+            else if opr aconvc \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
                     andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
             else FuncUtil.Ctermfunc.onefunc (ct, @1)
           end
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Limits.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -826,7 +826,7 @@
 
 lemma continuous_on_mult_const [simp]:
   fixes c::"'a::real_normed_algebra"
-  shows "continuous_on s (( *) c)"
+  shows "continuous_on s ((*) c)"
   by (intro continuous_on_mult_left continuous_on_id)
 
 lemma tendsto_divide_zero:
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1487,7 +1487,7 @@
 begin
 
 definition
-  times_matrix_def: "A * B = mult_matrix (( * )) (+) A B"
+  times_matrix_def: "A * B = mult_matrix ((*)) (+) A B"
 
 instance ..
 
@@ -1795,7 +1795,7 @@
 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
 
 definition scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" where
-  "scalar_mult a m == apply_matrix (( * ) a) m"
+  "scalar_mult a m == apply_matrix ((*) a) m"
 
 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
 by (simp add: scalar_mult_def)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Modules.thy
--- a/src/HOL/Modules.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Modules.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -878,9 +878,9 @@
 
 lemma module_hom_compose_scale:
   "module_hom s1 s2 (\<lambda>x. s2 (f x) (c))"
-  if "module_hom s1 ( *) f"
+  if "module_hom s1 (*) f"
 proof -
-  interpret mh: module_hom s1 "( *)" f by fact
+  interpret mh: module_hom s1 "(*)" f by fact
   show ?thesis
     by unfold_locales (simp_all add: mh.add mh.scale m2.scale_left_distrib)
 qed
@@ -913,7 +913,7 @@
   using module_axioms module_hom_iff scale_left_commute scale_right_distrib by blast
 
 lemma module_hom_scale_left[simp]:
-  "module_hom ( *) scale (\<lambda>r. scale r x)"
+  "module_hom (*) scale (\<lambda>r. scale r x)"
   by unfold_locales (auto simp: algebra_simps)
 
 lemma module_hom_id: "module_hom scale scale id"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Nonstandard_Analysis/HDeriv.thy
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -223,7 +223,7 @@
 lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1"
   by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
 
-lemma NSDERIV_cmult_Id [simp]: "NSDERIV (( * ) c) x :> c"
+lemma NSDERIV_cmult_Id [simp]: "NSDERIV ((*) c) x :> c"
   using NSDERIV_Id [THEN NSDERIV_cmult] by simp
 
 lemma NSDERIV_inverse:
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -413,7 +413,7 @@
 
 instantiation star :: (times) times
 begin
-  definition star_mult_def: "(( * )) \<equiv> *f2* (( * ))"
+  definition star_mult_def: "((*)) \<equiv> *f2* ((*))"
   instance ..
 end
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -731,7 +731,7 @@
 
 (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
 
-definition "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
+definition "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> (\<forall>p\<in> set ps. prime p)"
 
 lemma primefact:
   fixes n :: nat
@@ -743,8 +743,8 @@
   from assms have "n = prod_mset (prime_factorization n)"
     by (simp add: prod_mset_prime_factorization)
   also have "\<dots> = prod_mset (mset xs)" by (simp add: xs)
-  also have "\<dots> = foldr ( * ) xs 1" by (induct xs) simp_all
-  finally have "foldr ( * ) xs 1 = n" ..
+  also have "\<dots> = foldr (*) xs 1" by (induct xs) simp_all
+  finally have "foldr (*) xs 1 = n" ..
   moreover from xs have "\<forall>p\<in>#mset xs. prime p" by auto
   ultimately have "primefact xs n" by (auto simp: primefact_def)
   then show ?thesis ..
@@ -763,10 +763,10 @@
 next
   case (Cons q qs)
   from Cons.prems[unfolded primefact_def]
-  have q: "prime q" "q * foldr ( * ) qs 1 = n" "\<forall>p \<in>set qs. prime p"
-    and p: "prime p" "p dvd q * foldr ( * ) qs 1"
+  have q: "prime q" "q * foldr (*) qs 1 = n" "\<forall>p \<in>set qs. prime p"
+    and p: "prime p" "p dvd q * foldr (*) qs 1"
     by simp_all
-  consider "p dvd q" | "p dvd foldr ( * ) qs 1"
+  consider "p dvd q" | "p dvd foldr (*) qs 1"
     by (metis p prime_dvd_mult_eq_nat)
   then show ?case
   proof cases
@@ -776,19 +776,19 @@
     then show ?thesis by simp
   next
     case prem: 2
-    from q(3) have pqs: "primefact qs (foldr ( * ) qs 1)"
+    from q(3) have pqs: "primefact qs (foldr (*) qs 1)"
       by (simp add: primefact_def)
     from Cons.hyps[OF pqs p(1) prem] show ?thesis by simp
   qed
 qed
 
-lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr ( * ) ps 1 = n \<and> list_all prime ps"
+lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr (*) ps 1 = n \<and> list_all prime ps"
   by (auto simp add: primefact_def list_all_iff)
 
 text \<open>Variant of Lucas theorem.\<close>
 lemma lucas_primefact:
   assumes n: "n \<ge> 2" and an: "[a^(n - 1) = 1] (mod n)"
-    and psn: "foldr ( * ) ps 1 = n - 1"
+    and psn: "foldr (*) ps 1 = n - 1"
     and psp: "list_all (\<lambda>p. prime p \<and> \<not> [a^((n - 1) div p) = 1] (mod n)) ps"
   shows "prime n"
 proof -
@@ -806,7 +806,7 @@
 text \<open>Variant of Pocklington theorem.\<close>
 lemma pocklington_primefact:
   assumes n: "n \<ge> 2" and qrn: "q*r = n - 1" and nq2: "n \<le> q\<^sup>2"
-    and arnb: "(a^r) mod n = b" and psq: "foldr ( * ) ps 1 = q"
+    and arnb: "(a^r) mod n = b" and psq: "foldr (*) ps 1 = q"
     and bqn: "(b^q) mod n = 1"
     and psp: "list_all (\<lambda>p. prime p \<and> coprime ((b^(q div p)) mod n - 1) n) ps"
   shows "prime n"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Number_Theory/Totient.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -239,11 +239,11 @@
   assumes "prime p"
   shows   "totient (p ^ Suc n) = p ^ n * (p - 1)"
 proof -
-  from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - ( * ) p ` {0<..p ^ n})"
+  from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - (*) p ` {0<..p ^ n})"
     unfolding totient_def by (subst totatives_prime_power_Suc) simp_all
-  also from assms have "\<dots> = p ^ Suc n - card (( * ) p ` {0<..p^n})"
+  also from assms have "\<dots> = p ^ Suc n - card ((*) p ` {0<..p^n})"
     by (subst card_Diff_subset) (auto intro: prime_gt_0_nat)
-  also from assms have "card (( * ) p ` {0<..p^n}) = p ^ n"
+  also from assms have "card ((*) p ` {0<..p^n}) = p ^ n"
     by (subst card_image) (auto simp: inj_on_def)
   also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps)
   finally show ?thesis .
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1165,7 +1165,7 @@
   also have "...=  prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"
     by (auto intro!: indep_varD[where Ma=N and Mb=N])
   also have "... = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
-    by (auto intro!: arg_cong2[where f= "( * )"] arg_cong[where f= prob])
+    by (auto intro!: arg_cong2[where f= "(*)"] arg_cong[where f= prob])
   finally show ?thesis .
 qed
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Probability/PMF_Impl.thy
--- a/src/HOL/Probability/PMF_Impl.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -231,7 +231,7 @@
 qualified lemma mapping_of_bind_pmf:
   assumes "finite (set_pmf p)"
   shows   "mapping_of_pmf (bind_pmf p f) = 
-             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x)) 
+             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x)) 
                (mapping_of_pmf (f x))) (set_pmf p)"
   using assms
   by (intro mapping_of_pmfI')
@@ -268,7 +268,7 @@
 lemma bind_pmf_aux_code_aux:
   assumes "finite A"
   shows   "bind_pmf_aux p f A = 
-             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
+             fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
                (mapping_of_pmf (f x))) A" (is "?lhs = ?rhs")
 proof (intro mapping_eqI'[where d = 0])
   fix x assume "x \<in> Mapping.keys ?lhs"
@@ -287,7 +287,7 @@
 
 lemma bind_pmf_aux_code [code]:
   "bind_pmf_aux p f (set xs) = 
-     fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. ( * ) (pmf p x))
+     fold_combine_plus (\<lambda>x. Mapping.map_values (\<lambda>_. (*) (pmf p x))
                (mapping_of_pmf (f x))) (set xs)"
   by (rule bind_pmf_aux_code_aux) simp_all
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -78,7 +78,7 @@
 done
 
 quotient_definition
-  "(( * )) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+  "((*)) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
   apply(rule equivp_transp[OF int_equivp])
   apply(rule times_int_raw_fst)
   apply(assumption)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -41,7 +41,7 @@
   "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
 
 quotient_definition
-  "(( * )) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute)
+  "((*)) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute)
 
 fun plus_rat_raw where
   "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -32,7 +32,7 @@
   for x :: "'a::cancel_semigroup_add"
   by (meson add_left_imp_eq injI)
 
-lemma inj_mult_left [simp]: "inj (( * ) x) \<longleftrightarrow> x \<noteq> 0"
+lemma inj_mult_left [simp]: "inj ((*) x) \<longleftrightarrow> x \<noteq> 0"
   for x :: "'a::idom"
   by (metis injI mult_cancel_left the_inv_f_f zero_neq_one)
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -603,7 +603,7 @@
     hence "(\<lambda>n. (-(x^2))^n) sums (1 / (1 - (-(x^2))))" by (intro geometric_sums) simp_all
     also have "1 - (-(x^2)) = 1 + x^2" by simp
     also have "(\<lambda>n. (-(x^2))^n) = (\<lambda>n. ?f (2*n))" by (auto simp: fun_eq_iff power_minus' power_mult)
-    also have "range (( *) (2::nat)) = {n. even n}"
+    also have "range ((*) (2::nat)) = {n. even n}"
       by (auto elim!: evenE)
     hence "(\<lambda>n. ?f (2*n)) sums (1 / (1 + x^2)) \<longleftrightarrow> ?f sums (1 / (1 + x^2))"
       by (intro sums_mono_reindex) (simp_all add: strict_mono_Suc_iff)
@@ -1225,11 +1225,11 @@
       | (xs, MSLNil) \<Rightarrow> MSLNil
       | (MSLCons x xs, MSLCons y ys) \<Rightarrow>
            MSLCons (fst x * fst y, snd x + snd y) 
-             (plus_ms_aux (mslmap (map_prod (( *) (fst x)) ((+) (snd x))) ys)
+             (plus_ms_aux (mslmap (map_prod ((*) (fst x)) ((+) (snd x))) ys)
                (times_ms_aux xs (MSLCons y ys))))"
 
 definition scale_shift_ms_aux :: "('a :: times \<times> real) \<Rightarrow> ('a \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
-  "scale_shift_ms_aux = (\<lambda>(a,b) xs. mslmap (map_prod (( *) a) ((+) b)) xs)"
+  "scale_shift_ms_aux = (\<lambda>(a,b) xs. mslmap (map_prod ((*) a) ((+) b)) xs)"
 
 lemma times_ms_aux_altdef:
   "times_ms_aux xs ys = 
@@ -1282,7 +1282,7 @@
 qed
 
 lemma scale_shift_ms_aux_conv_mslmap: 
-  "scale_shift_ms_aux x = mslmap (map_prod (( *) (fst x)) ((+) (snd x)))"
+  "scale_shift_ms_aux x = mslmap (map_prod ((*) (fst x)) ((+) (snd x)))"
   by (rule ext) (simp add: scale_shift_ms_aux_def map_prod_def case_prod_unfold)
 
 fun inverse_ms_aux :: "('a :: multiseries \<times> real) msllist \<Rightarrow> ('a \<times> real) msllist" where
@@ -2525,7 +2525,7 @@
   have "times_ms_aux (MSLCons (const_expansion 1, 0) MSLNil) xs = xs" for xs :: "('a \<times> real) msllist"
   proof (coinduction arbitrary: xs rule: msllist.coinduct_upto)
     case Eq_real_prod_msllist
-    have "map_prod (( *) (const_expansion 1 :: 'a)) ((+) (0::real)) = (\<lambda>x. x)"
+    have "map_prod ((*) (const_expansion 1 :: 'a)) ((+) (0::real)) = (\<lambda>x. x)"
       by (rule ext) (simp add: map_prod_def times_const_expansion_1 case_prod_unfold)
     moreover have "mslmap \<dots> = (\<lambda>x. x)" by (rule ext) (simp add: msllist.map_ident)
     ultimately have "scale_shift_ms_aux (const_expansion 1 :: 'a, 0) = (\<lambda>x. x)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Real_Asymp/Real_Asymp_Approx.thy
--- a/src/HOL/Real_Asymp/Real_Asymp_Approx.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/Real_Asymp_Approx.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -39,7 +39,7 @@
 
 fun eval_nat (@{term "(+) :: nat => _"} $ a $ b) = bin (op +) (a, b)
   | eval_nat (@{term "(-) :: nat => _"} $ a $ b) = bin (clamp o op -) (a, b)
-  | eval_nat (@{term "( * ) :: nat => _"} $ a $ b) = bin (op *) (a, b)
+  | eval_nat (@{term "(*) :: nat => _"} $ a $ b) = bin (op *) (a, b)
   | eval_nat (@{term "(div) :: nat => _"} $ a $ b) = bin Int.div (a, b)
   | eval_nat (@{term "(^) :: nat => _"} $ a $ b) = bin (fn (a,b) => Integer.pow a b) (a, b)
   | eval_nat (t as (@{term "numeral :: _ => nat"} $ _)) = snd (HOLogic.dest_number t)
@@ -65,7 +65,7 @@
 
 fun eval (@{term "(+) :: real => _"} $ a $ b) = eval a + eval b
   | eval (@{term "(-) :: real => _"} $ a $ b) = eval a - eval b
-  | eval (@{term "( * ) :: real => _"} $ a $ b) = eval a * eval b
+  | eval (@{term "(*) :: real => _"} $ a $ b) = eval a * eval b
   | eval (@{term "(/) :: real => _"} $ a $ b) =
       let val a = eval a; val b = eval b in
         if Real.==(b, Real.fromInt 0) then nan else a / b
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Real_Asymp/exp_log_expression.ML
--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -257,7 +257,7 @@
       | expr_to_term' (Add (a, b)) = 
           @{term "(+) :: real => _"} $ expr_to_term' a $ expr_to_term' b
       | expr_to_term' (Mult (a, b)) = 
-          @{term "( *) :: real => _"} $ expr_to_term' a $ expr_to_term' b
+          @{term "(*) :: real => _"} $ expr_to_term' a $ expr_to_term' b
       | expr_to_term' (Minus (a, b)) = 
           @{term "(-) :: real => _"} $ expr_to_term' a $ expr_to_term' b
       | expr_to_term' (Div (a, b)) = 
@@ -354,7 +354,7 @@
           Add (reify' s, reify' t)
       | reify'' (@{term "(-) :: real => _"} $ s $ t) =
           Minus (reify' s, reify' t)
-      | reify'' (@{term "( *) :: real => _"} $ s $ t) =
+      | reify'' (@{term "(*) :: real => _"} $ s $ t) =
           Mult (reify' s, reify' t)
       | reify'' (@{term "(/) :: real => _"} $ s $ t) =
           Div (reify' s, reify' t)
@@ -435,7 +435,7 @@
           Add (reify'' s, reify'' t)
       | reify'' (@{term "(-) :: real => _"} $ s $ t) =
           Minus (reify'' s, reify'' t)
-      | reify'' (@{term "( *) :: real => _"} $ s $ t) =
+      | reify'' (@{term "(*) :: real => _"} $ s $ t) =
           Mult (reify'' s, reify'' t)
       | reify'' (@{term "(/) :: real => _"} $ s $ t) =
           Div (reify'' s, reify'' t)
@@ -509,7 +509,7 @@
       "(" ^ simple_print_const a ^ "+" ^ simple_print_const b ^ ")"
   | simple_print_const (@{term "(-) :: real => _"} $ a $ b) =
       "(" ^ simple_print_const a ^ "-" ^ simple_print_const b ^ ")"
-  | simple_print_const (@{term "( * ) :: real => _"} $ a $ b) =
+  | simple_print_const (@{term "(*) :: real => _"} $ a $ b) =
       "(" ^ simple_print_const a ^ "*" ^ simple_print_const b ^ ")"
   | simple_print_const (@{term "inverse :: real => _"} $ a) =
       "(1 / " ^ simple_print_const a ^ ")"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Real_Asymp/multiseries_expansion.ML
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -2262,7 +2262,7 @@
       else if b aconv @{term "\<lambda>_::real. -1 :: real"} then
         Term.betapply (@{term "\<lambda>(f::real\<Rightarrow>real) x. -f x"}, a)
       else
-        Abs ("x", @{typ real}, @{term "( *) :: real => _"} $
+        Abs ("x", @{typ real}, @{term "(*) :: real => _"} $
           (Term.betapply (a, Bound 0)) $ (Term.betapply (b, Bound 0)))
 
     fun mk_powr b e =
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -53,8 +53,8 @@
 end
 
 global_interpretation real_vector?: vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
-  rewrites "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
-    and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
+  rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
+    and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
   defines dependent_raw_def: dependent = real_vector.dependent
     and representation_raw_def: representation = real_vector.representation
     and subspace_raw_def: subspace = real_vector.subspace
@@ -82,8 +82,8 @@
 abbreviation "independent x \<equiv> \<not> dependent x"
 
 global_interpretation real_vector?: vector_space_pair "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
-  rewrites  "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
-    and "Vector_Spaces.linear ( *) ( *\<^sub>R) = linear"
+  rewrites  "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
+    and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
   defines construct_raw_def: construct = real_vector.construct
   apply unfold_locales
   unfolding linear_def real_scaleR_def
@@ -1316,7 +1316,7 @@
 
 corollary real_linearD:
   fixes f :: "real \<Rightarrow> real"
-  assumes "linear f" obtains c where "f = ( *) c"
+  assumes "linear f" obtains c where "f = (*) c"
   by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
 
 lemma linear_times_of_real: "linear (\<lambda>x. a * of_real x)"
@@ -1439,7 +1439,7 @@
 
 lemma comp1:
   assumes "bounded_linear g"
-  shows "bounded_bilinear (\<lambda>x. ( **) (g x))"
+  shows "bounded_bilinear (\<lambda>x. (**) (g x))"
 proof unfold_locales
   interpret g: bounded_linear g by fact
   show "\<And>a a' b. g (a + a') ** b = g a ** b + g a' ** b"
@@ -1537,7 +1537,7 @@
   qed
 qed
 
-lemma bounded_bilinear_mult: "bounded_bilinear (( *) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
+lemma bounded_bilinear_mult: "bounded_bilinear ((*) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
   apply (rule bounded_bilinear.intro)
       apply (auto simp: algebra_simps)
   apply (rule_tac x=1 in exI)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/SMT.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -134,7 +134,7 @@
 lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
 lemma nat_plus_as_int: "(+) = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
 lemma nat_minus_as_int: "(-) = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
-lemma nat_times_as_int: "( * ) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
+lemma nat_times_as_int: "(*) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
 lemma nat_div_as_int: "(div) = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
 lemma nat_mod_as_int: "(mod) = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/SMT_Examples/boogie.ML
--- a/src/HOL/SMT_Examples/boogie.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -139,7 +139,7 @@
       parse_bin_expr cx (mk_binary @{term "(<=) :: int => _"} o swap) ls
   | parse_expr cx (["+"] :: ls) = parse_bin_expr cx (mk_binary @{term "(+) :: int => _"}) ls
   | parse_expr cx (["-"] :: ls) = parse_bin_expr cx (mk_binary @{term "(-) :: int => _"}) ls
-  | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "( * ) :: int => _"}) ls
+  | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary @{term "(*) :: int => _"}) ls
   | parse_expr cx (["/"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_div}) ls
   | parse_expr cx (["%"] :: ls) = parse_bin_expr cx (mk_binary @{term boogie_mod}) ls
   | parse_expr cx (["select", n] :: ls) =
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -1015,12 +1015,12 @@
 context linordered_field begin
 
 lemma image_mult_atLeastAtMost [simp]:
-  "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
+  "((*) d ` {a..b}) = {d*a..d*b}" if "d>0"
   using that
   by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
 
 lemma image_mult_atLeastAtMost_if:
-  "( * ) c ` {x .. y} =
+  "(*) c ` {x .. y} =
     (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
 proof -
   consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
@@ -1028,7 +1028,7 @@
   then show ?thesis
   proof cases
     case 1
-    have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
+    have "(*) c ` {x .. y} = uminus ` (*) (- c) ` {x .. y}"
       by (simp add: image_image)
     also have "\<dots> = {c * y .. c * x}"
       using \<open>c < 0\<close>
@@ -1049,7 +1049,7 @@
             else if 0 \<le> m then {m*a + c .. m *b + c}
             else {m*b + c .. m*a + c})"
 proof -
-  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
+  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o (*) m)"
     unfolding image_comp[symmetric]
     by (simp add: o_def)
   then show ?thesis
@@ -2474,7 +2474,7 @@
 lemma prod_atLeastAtMost_code:
   "prod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
 proof -
-  have "comp_fun_commute (\<lambda>a. ( * ) (f a))"
+  have "comp_fun_commute (\<lambda>a. (*) (f a))"
     by unfold_locales (auto simp: o_def mult_ac)
   thus ?thesis
     by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/TLA/Intensional.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -119,7 +119,7 @@
   "_liftIf"       == "_lift3 (CONST If)"
   "_liftPlus"     == "_lift2 (+)"
   "_liftMinus"    == "_lift2 (-)"
-  "_liftTimes"    == "_lift2 (( * ))"
+  "_liftTimes"    == "_lift2 ((*))"
   "_liftDiv"      == "_lift2 (div)"
   "_liftMod"      == "_lift2 (mod)"
   "_liftLess"     == "_lift2 (<)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -23,7 +23,7 @@
 val allowed_consts =
   [@{term "(+) :: int => _"}, @{term "(+) :: nat => _"},
    @{term "(-) :: int => _"}, @{term "(-) :: nat => _"},
-   @{term "( * ) :: int => _"}, @{term "( * ) :: nat => _"},
+   @{term "(*) :: int => _"}, @{term "(*) :: nat => _"},
    @{term "(div) :: int => _"}, @{term "(div) :: nat => _"},
    @{term "(mod) :: int => _"}, @{term "(mod) :: nat => _"},
    @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
@@ -171,7 +171,7 @@
 val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP;
 
 val cadd =  @{cterm "(+) :: int => _"}
-val cmulC =  @{cterm "( * ) :: int => _"}
+val cmulC =  @{cterm "(*) :: int => _"}
 val cminus =  @{cterm "(-) :: int => _"}
 val cone =  @{cterm "1 :: int"}
 val [addC, mulC, subC] = map Thm.term_of [cadd, cmulC, cminus]
@@ -662,7 +662,7 @@
   | term_of_num vs (Proc.Sub (t1, t2)) =
       @{term "(-) :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
   | term_of_num vs (Proc.Mul (i, t2)) =
-      @{term "( * ) :: int => _"} $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2
+      @{term "(*) :: int => _"} $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2
   | term_of_num vs (Proc.CN (n, i, t')) =
       term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
 
@@ -765,7 +765,7 @@
   if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t))
   then false
   else case Thm.term_of t of
-    c$l$r => if member (op =) [@{term"( * )::int => _"}, @{term"( * )::nat => _"}] c
+    c$l$r => if member (op =) [@{term"(*)::int => _"}, @{term"(*)::nat => _"}] c
              then not (isnum l orelse isnum r)
              else not (member (op aconv) cts c)
   | c$_ => not (member (op aconv) cts c)
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -61,13 +61,13 @@
 definition dependent :: "'b set \<Rightarrow> bool"
   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)))"
 
-lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 ( *s) = subspace"
+lemma implicit_subspace_with[implicit_ab_group_add]: "subspace_with (+) 0 (*s) = subspace"
   unfolding subspace_on_def subspace_with_def ..
 
-lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 ( *s) = dependent"
+lemma implicit_dependent_with[implicit_ab_group_add]: "dependent_with (+) 0 (*s) = dependent"
   unfolding dependent_on_def dependent_with_def sum_with ..
 
-lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 ( *s) = span"
+lemma implicit_span_with[implicit_ab_group_add]: "span_with (+) 0 (*s) = span"
   unfolding span_on_def span_with_def sum_with ..
 
 end
@@ -109,7 +109,7 @@
     then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V)
     else 0)"
 
-lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 ( *s) = dim"
+lemma implicit_dim_with[implicit_ab_group_add]: "dim_on_with S (+) 0 (*s) = dim"
   unfolding dim_on_with_def dim_def implicit_ab_group_add ..
 
 end
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Vector_Spaces.thy
--- a/src/HOL/Vector_Spaces.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Vector_Spaces.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -77,10 +77,10 @@
 
 lemma linear_imp_scale:
   fixes D::"'a \<Rightarrow> 'b"
-  assumes "linear ( *) scale D"
+  assumes "linear (*) scale D"
   obtains d where "D = (\<lambda>x. scale x d)"
 proof -
-  interpret linear "( *)" scale D by fact
+  interpret linear "(*)" scale D by fact
   show ?thesis
     by (metis mult.commute mult.left_neutral scale that)
 qed
@@ -806,7 +806,7 @@
 lemma in_span_in_range_construct:
   "x \<in> range (construct B f)" if i: "vs1.independent B" and x: "x \<in> vs2.span (f ` B)"
 proof -
-  interpret linear "( *a)" "( *b)" "construct B f"
+  interpret linear "(*a)" "(*b)" "construct B f"
     using i by (rule linear_construct)
   obtain bb :: "('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'b set \<Rightarrow> 'b" where
     "\<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))"
@@ -853,7 +853,7 @@
     have fB: "vs2.independent (f ` B)"
       using independent_injective_image[OF B f] .
     let ?g = "p.construct (f ` B) (the_inv_into B f)"
-    show "linear ( *b) ( *a) ?g"
+    show "linear (*b) (*a) ?g"
       by (rule p.linear_construct[OF fB])
     have "?g b \<in> vs1.span (the_inv_into B f ` f ` B)" for b
       by (intro p.construct_in_span fB)
@@ -864,13 +864,13 @@
       by (auto simp: V_eq)
     have "(?g \<circ> f) v = id v" if "v \<in> vs1.span B" for v
     proof (rule vector_space_pair.linear_eq_on[where x=v])
-      show "vector_space_pair ( *a) ( *a)" by unfold_locales
-      show "linear ( *a) ( *a) (?g \<circ> f)"
-      proof (rule Vector_Spaces.linear_compose[of _ "( *b)"])
-        show "linear ( *a) ( *b) f"
+      show "vector_space_pair (*a) (*a)" by unfold_locales
+      show "linear (*a) (*a) (?g \<circ> f)"
+      proof (rule Vector_Spaces.linear_compose[of _ "(*b)"])
+        show "linear (*a) (*b) f"
           by unfold_locales
       qed fact
-      show "linear ( *a) ( *a) id" by (rule vs1.linear_id)
+      show "linear (*a) (*a) id" by (rule vs1.linear_id)
       show "v \<in> vs1.span B" by fact
       show "b \<in> B \<Longrightarrow> (p.construct (f ` B) (the_inv_into B f) \<circ> f) b = id b" for b
         by (simp add: p.construct_basis fB the_inv_into_f_f inj_on_subset[OF f vs1.span_superset])
@@ -895,7 +895,7 @@
   proof (intro exI ballI conjI)
     interpret p: vector_space_pair s2 s1 by unfold_locales
     let ?g = "p.construct C g"
-    show "linear ( *b) ( *a) ?g"
+    show "linear (*b) (*a) ?g"
       by (rule p.linear_construct[OF C])
     have "?g v \<in> vs1.span (g ` C)" for v
       by (rule p.construct_in_span[OF C])
@@ -903,10 +903,10 @@
     finally show "?g ` UNIV \<subseteq> V" by auto
     have "(f \<circ> ?g) v = id v" if v: "v \<in> f ` V" for v
     proof (rule vector_space_pair.linear_eq_on[where x=v])
-      show "vector_space_pair ( *b) ( *b)" by unfold_locales
-      show "linear ( *b) ( *b) (f \<circ> ?g)"
-        by (rule Vector_Spaces.linear_compose[of _ "( *a)"]) fact+
-      show "linear ( *b) ( *b) id" by (rule vs2.linear_id)
+      show "vector_space_pair (*b) (*b)" by unfold_locales
+      show "linear (*b) (*b) (f \<circ> ?g)"
+        by (rule Vector_Spaces.linear_compose[of _ "(*a)"]) fact+
+      show "linear (*b) (*b) id" by (rule vs2.linear_id)
       have "vs2.span (f ` B) = vs2.span C"
         using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
         by auto
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/Word/Word.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -273,7 +273,7 @@
 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
   by (auto simp add: bintrunc_mod2p intro: mod_minus_cong)
 
-lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "( * )"
+lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(*)"
   by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
 
 definition word_div_def: "a div b = word_of_int (uint a div uint b)"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -738,7 +738,7 @@
 
 
 locale Dgrp = Dmonoid +
-  assumes unit [intro, simp]: "Dmonoid.unit (( ** )) one x"
+  assumes unit [intro, simp]: "Dmonoid.unit ((**)) one x"
 
 begin
 
diff -r 765ff343a7aa -r 5ed7206dbf18 src/HOL/ex/Transfer_Int_Nat.thy
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Mon Sep 24 23:49:43 2018 +0200
@@ -38,7 +38,7 @@
 lemma ZN_add [transfer_rule]: "(ZN ===> ZN ===> ZN) (+) (+)"
   unfolding rel_fun_def ZN_def by simp
 
-lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) (( * )) (( * ))"
+lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) ((*)) ((*))"
   unfolding rel_fun_def ZN_def by simp
 
 definition tsub :: "int \<Rightarrow> int \<Rightarrow> int"
diff -r 765ff343a7aa -r 5ed7206dbf18 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Mon Sep 24 22:10:24 2018 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Mon Sep 24 23:49:43 2018 +0200
@@ -172,12 +172,8 @@
 val binder_name = suffix "_binder";
 
 fun mk_prefix sy =
-  let
-    fun star1 sys = (fst(hd sys) = "*");
-    val sy' = Input.source_explode (Input.reset_pos sy); 
-    val lpar = Symbol_Pos.explode0 ("'(" ^ (if star1 sy' then " " else ""));
-    val rpar = Symbol_Pos.explode0 ((if star1(rev sy') then " " else "") ^ "')")
- in lpar @ sy' @ rpar end
+  let val sy' = Input.source_explode (Input.reset_pos sy); 
+  in Symbol_Pos.explode0 "'(" @ sy' @ Symbol_Pos.explode0 "')" end
 
 fun syn_ext_consts logical_types const_decls =
   let