%% $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}