# HG changeset patch
# User blanchet
# Date 1355953491 -3600
# Node ID 69b22c4398fea1af1b559aebf71c849d5f28eb44
# Parent  4f840e2e362ec68697f5b11bc1a223db78b20c42# Parent  620515b73a77f73fadd71f251654c53011819839
more

diff -r 4f840e2e362e -r 69b22c4398fe src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Wed Dec 19 22:43:07 2012 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Wed Dec 19 22:44:51 2012 +0100
@@ -590,30 +590,38 @@
 \section*{Infix operators in Main} % @{theory Main}
 
 \begin{center}
-\begin{tabular}{lll}
-Operator & precedence & associativity \\
-@{text"="}, @{text"\<noteq>"} & 50 & left\\
-@{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
-@{text"\<and>"} & 35 & right \\
-@{text"\<or>"} & 30 & right \\
-@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
-@{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
-@{text"\<in>"}, @{text"\<notin>"} & 50 \\
-@{text"\<inter>"} & 70 & left \\
-@{text"\<union>"} & 65 & left \\
-@{text"\<circ>"} & 55 & left\\
-@{text"`"} & 90 & right\\
-@{text"O"} & 75 & right\\
-@{text"``"} & 90 & right\\
-@{text"+"}, @{text"-"} & 65 & left \\
-@{text"*"}, @{text"/"} & 70 & left \\
-@{text"div"}, @{text"mod"} & 70 & left\\
-@{text"^"} & 80 & right\\
-@{text"^^"} & 80 & right\\
-@{text"dvd"} & 50 \\
-@{text"#"}, @{text"@"} & 65 & right\\
-@{text"!"} & 100 & left\\
-@{text"++"} & 100 & left\\
+\begin{tabular}{llll}
+ & Operator & precedence & associativity \\
+\hline
+Meta-logic & @{text"\<Longrightarrow>"} & 1 & right \\
+& @{text"\<equiv>"} & 2 \\
+\hline
+Logic & @{text"\<and>"} & 35 & right \\
+&@{text"\<or>"} & 30 & right \\
+&@{text"\<longrightarrow>"}, @{text"\<longleftrightarrow>"} & 25 & right\\
+&@{text"="}, @{text"\<noteq>"} & 50 & left\\
+\hline
+Orderings & @{text"\<le>"}, @{text"<"}, @{text"\<ge>"}, @{text">"} & 50 \\
+\hline
+Sets & @{text"\<subseteq>"}, @{text"\<subset>"}, @{text"\<supseteq>"}, @{text"\<supset>"} & 50 \\
+&@{text"\<in>"}, @{text"\<notin>"} & 50 \\
+&@{text"\<inter>"} & 70 & left \\
+&@{text"\<union>"} & 65 & left \\
+\hline
+Functions and Relations & @{text"\<circ>"} & 55 & left\\
+&@{text"`"} & 90 & right\\
+&@{text"O"} & 75 & right\\
+&@{text"``"} & 90 & 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\\
+&@{text"!"} & 100 & left
 \end{tabular}
 \end{center}
 *}