--- a/src/Doc/Main/Main_Doc.thy Thu Jul 17 14:55:56 2014 +0200
+++ b/src/Doc/Main/Main_Doc.thy Fri Jul 18 14:03:09 2014 +0200
@@ -612,12 +612,12 @@
&@{text"`"} & 90 & right\\
&@{text"O"} & 75 & right\\
&@{text"``"} & 90 & right\\
+&@{text"^^"} & 80 & right\\
\hline
Numbers & @{text"+"}, @{text"-"} & 65 & left \\
&@{text"*"}, @{text"/"} & 70 & left \\
&@{text"div"}, @{text"mod"} & 70 & left\\
&@{text"^"} & 80 & right\\
-&@{text"^^"} & 80 & right\\
&@{text"dvd"} & 50 \\
\hline
Lists & @{text"#"}, @{text"@"} & 65 & right\\