doc-src/Ref/defining.tex

updated section on raw syntax;
misc tuning;

\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: