\documentclass[a4paper]{article}
\usepackage[margin=1in]{geometry}
\usepackage{hyperref}

\usepackage{amssymb}
\usepackage{stmaryrd}

\title{}
\author{}

\begin{document}

\begin{table}[h]
{\em Operator precedence cheat sheet for Isabelle/HOL} (quick and dirty, little quality control, version 2012-Nov-12). Follow-up of the discussion at the Isabelle mailing list in November 2012, \url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00020.html}.  Entries without a fixed precedence are still rough guesstimates (that may need further correction).
\begin{center}

\begin{tabular}{|l|r|p{6cm}|}
\hline
Class & Precedence & Symbols and the minimum precedence of symbols that may be contained in non-terminals \\
\hline
\hline function &      & application of user-defined function, field dereference (record) \\
\hline function &  900 & (900 $\llparenthesis$ 0 $\rrparenthesis$ (record update)) \\ 
\hline function &  100 & (100 nth (list) 101) \\ 
\hline type	    &      & ``set'' type constructor, ``list'' type constructor \\
\hline function &   70 & (70 $\cap$ (set) 71), (70 * (nat) 71) \\
\hline function &   65 & (65 $\cup$ (set) 66), (65 + (nat) 66), (65 $-$ (nat) 66), (66 \# (list) 65), (66 @ (list) 65) \\
\hline relation &   50 & (50 = 51), (50 $\in$ 51), (51 $<$ 51), (51 $\le$ 51) \\ 
\hline logic    &   40 & ($\neg$ 40) \\ 
\hline logic    &   35 & (36 $\wedge$ 35) \\
\hline logic    &   30 & (31 $\vee$ 30) \\
\hline logic    &   25 & (26 $\longrightarrow$ 25), (26 $\leftrightarrow$ 25) \\
\hline logic    &   10 & ($\forall$ 0 .\ 10), ($\exists$ 0 .\ 10), (if 0 then 0 else 10), (case 0 of 10), (let 0 in 10) \\
\hline type	    &    3 & (4 :: 0)  \\
\hline logic    &    3 & ($\lambda $ 0 .\ 3) \\
\hline metalogic &   2 & (3 $\equiv$ 2) \\
\hline metalogic &   1 & (2 $\Longrightarrow$ 1) \\
\hline type	    &    0 & (1 $\Rightarrow$ 0) \\
\hline metalogic &   0 & ($\bigwedge$ 0 .\ 0) \\
\hline

\end{tabular}
\caption{Higher symbols have higher precedence. Precedences given where known to me, by use of the Isabelle command ``print\_syntax'' - you can issue this command for example anywhere in an empty theory or an existing theory. ``print\_syntax'' also shows precedence for a lot of symbols not given in the table for brevity (say, exponentiation of natural numbers). Following the convention of the output of ``print\_syntax'', associativity of binary operators is determined by that a non-terminal in the right-hand side production rule of a grammar only may be expanded by non-terminals with the same or higher precedence. Hence, for example addition on the natural numbers is left-associative, as its production still allows expansion to the left of the ``+'' operator. Conversely, for example list concatenation is right-associative. ``$<$'' is not associative at all (no expansion allowed either way). See also the post by Holger Gast for a more detailed explanation (\url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00032.html}). Classes are my own interpretation.} 
\end{center}
\end{table}

\paragraph{Note on classes:}

\begin{description}
\item[function] if it is a function (type constructors ``set'', ``list'' could also be seen as functions)
\item[relation] if it is a relation
\item[logic] if it is object logic
\item[metalogic] if it is meta logic
\end{description}

\end{document}
