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