%% $Id$

\appendix

\newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem

\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}

\begin{itemize}

\item {\tt Typewriter font} denotes terminal symbols.

\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of

  identifiers, type identifiers, natural numbers, \ML\ strings (with their

  quotation marks) and arbitrary \ML\ text.  The first three are fully defined

  in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.

\end{itemize}

\begin{rail}

theoryDef : id '=' (name + '+') ('+' extension | ());

name: id | string;

extension : classes default types arities consts trans rules 'end' ml

          ;

classes : ()

        | 'classes' ( ( id (  ()

                            | '<' (id + ',')

                           ) 

                       ) + )

        ;

default : ()

        | 'default' sort 

        ;

sort :  id

     | '\{' (id * ',') '\}'

     ;

types :  ()

      | 'types' ( ( type ( () | '(' infix ')' ) ) + )

      ;

type : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '='  string );

infix : ( 'infixr' | 'infixl' ) nat;

arities :  ()

        | 'arities' ((( name + ',' ) '::' arity ) + )

        ;

arity   : ( () 

          | '(' (sort + ',') ')' 

          ) id

        ;

consts :  ()

       | 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )

       ;

constDecl : ( name + ',') '::' string ;

mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )

       | infix

       | 'binder' string nat ;

trans : ()

      | 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )

      ;

pat : ( () | ( '(' id ')' ) ) string;

rules :  ()

      | 'rules' (( id string ) + )

      ;

ml :  ()

   | 'ML' text

   ;

\end{rail}