\chapter{Defining Logics} \label{Defining-Logics}
\section{Mixfix declarations} \label{sec:mixfix}
\subsection{Example: arithmetic expressions}
\index{examples!of mixfix declarations}
This theory specification contains a {\tt syntax} section with mixfix
declarations encoding the priority grammar from
\S\ref{sec:priority_grammars}:
\begin{ttbox}
ExpSyntax = Pure +
types
exp
syntax
"0" :: exp ("0" 9)
"+" :: [exp, exp] => exp ("_ + _" [0, 1] 0)
"*" :: [exp, exp] => exp ("_ * _" [3, 2] 2)
"-" :: exp => exp ("- _" [3] 3)
end
\end{ttbox}
Executing {\tt Syntax.print_gram} reveals the productions derived from the
above mixfix declarations (lots of additional information deleted):
\begin{ttbox}
Syntax.print_gram (syn_of ExpSyntax.thy);
{\out exp = "0" => "0" (9)}
{\out exp = exp[0] "+" exp[1] => "+" (0)}
{\out exp = exp[3] "*" exp[2] => "*" (2)}
{\out exp = "-" exp[3] => "-" (3)}
\end{ttbox}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
%%% End: