# HG changeset patch # User nipkow # Date 1355953464 -3600 # Node ID 620515b73a77f73fadd71f251654c53011819839 # Parent 3e3c2af5e8a52cac94e1c4a19a20bec4ba8484a7 tuned infix table diff -r 3e3c2af5e8a5 -r 620515b73a77 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Wed Dec 19 22:26:26 2012 +0100 +++ b/src/Doc/Main/Main_Doc.thy Wed Dec 19 22:44:24 2012 +0100 @@ -590,30 +590,38 @@ \section*{Infix operators in Main} % @{theory Main} \begin{center} -\begin{tabular}{lll} -Operator & precedence & associativity \\ -@{text"="}, @{text"\"} & 50 & left\\ -@{text"\"}, @{text"<"}, @{text"\"}, @{text">"} & 50 \\ -@{text"\"} & 35 & right \\ -@{text"\"} & 30 & right \\ -@{text"\"}, @{text"\"} & 25 & right\\ -@{text"\"}, @{text"\"}, @{text"\"}, @{text"\"} & 50 \\ -@{text"\"}, @{text"\"} & 50 \\ -@{text"\"} & 70 & left \\ -@{text"\"} & 65 & left \\ -@{text"\"} & 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"\"} & 1 & right \\ +& @{text"\"} & 2 \\ +\hline +Logic & @{text"\"} & 35 & right \\ +&@{text"\"} & 30 & right \\ +&@{text"\"}, @{text"\"} & 25 & right\\ +&@{text"="}, @{text"\"} & 50 & left\\ +\hline +Orderings & @{text"\"}, @{text"<"}, @{text"\"}, @{text">"} & 50 \\ +\hline +Sets & @{text"\"}, @{text"\"}, @{text"\"}, @{text"\"} & 50 \\ +&@{text"\"}, @{text"\"} & 50 \\ +&@{text"\"} & 70 & left \\ +&@{text"\"} & 65 & left \\ +\hline +Functions and Relations & @{text"\"} & 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} *}