# HG changeset patch
# User nipkow
# Date 1537798167 -7200
# Node ID 440f7a575760817cda155ce506d869dde6edba03
# Parent  5840724b1d71139a62d68e10450f4c2d3e97da79
more conversion from ( * ) to (*)

diff -r 5840724b1d71 -r 440f7a575760 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 24 14:30:09 2018 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Sep 24 16:09:27 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 5840724b1d71 -r 440f7a575760 src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Mon Sep 24 14:30:09 2018 +0200
+++ b/src/Doc/Locales/Examples3.thy	Mon Sep 24 16:09:27 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 5840724b1d71 -r 440f7a575760 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Mon Sep 24 14:30:09 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Mon Sep 24 16:09:27 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 5840724b1d71 -r 440f7a575760 src/HOL/SMT_Examples/boogie.ML
--- a/src/HOL/SMT_Examples/boogie.ML	Mon Sep 24 14:30:09 2018 +0200
+++ b/src/HOL/SMT_Examples/boogie.ML	Mon Sep 24 16:09:27 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) =