--- 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>
--- 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"
--- 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"}&
--- 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) =