# HG changeset patch
# User nipkow
# Date 1405684989 -7200
# Node ID 70fcc642839300ab5955605822fc1703211cc2f9
# Parent  e20a999f7161f12f3c37a638fe67107b83c89bc1
tuned

diff -r e20a999f7161 -r 70fcc6428393 src/Doc/Main/Main_Doc.thy
--- 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\\