%% $Id$

 \appendix

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

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

 Below we present the full syntax of theory definition files as

 provided by {\Pure} Isabelle --- object-logics may add their own

 sections.  \S\ref{sec:ref-defining-theories} explains the meanings of

 these constructs.  The syntax obeys the following conventions:

 \begin{itemize}

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

 \item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical

   classes of identifiers, type identifiers, natural numbers, quoted

   strings (without the need for \verb$\$\dots\verb$\$ between lines)

   and long qualified \ML{} identifiers.

   The categories $id$, $tid$, $nat$ are fully defined in \iflabelundefined{Defining-Logics}%

   {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%

   {\S\ref{Defining-Logics}}.

 \item $text$ is all text from the current position to the end of file,

   $verbatim$ is any text enclosed in \verb.{|.\dots\verb.|}.

 \item Comments in theories take the form {\tt (*}\dots{\tt*)} and may

   be nested, just as in \ML.

 \end{itemize}

 \begin{rail}

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

           ;

 name: id | string

     ;

 extension : (section +) 'end' ( () | ml )

           ;

 section : classes

         | default

         | types

         | arities

         | consts

         | syntax

         | trans

         | defs

         | constdefs

         | rules

         | axclass

         | instance

         | oracle

         ;

 classes : 'classes' ( classDecl + )

         ;

 classDecl : (id (() | '<' (id + ',')))

         ;

 default : 'default' sort 

         ;

 sort :  id

      | lbrace (id * ',') rbrace

      ;

 types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )

       ;

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

       ;

 typeDecl : typevarlist name

            ( () | '=' ( string | type ) );

 typevarlist : () | tid | '(' ( tid + ',' ) ')';

 type : simpleType | '(' type ')' | type '=>' type |

        '[' ( type + "," ) ']' '=>' type;

 simpleType: id | ( tid ( () | '::' id ) ) |

             '(' ( type + "," ) ')' id | simpleType id

           ;

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

         ;

 arity : ( () | '(' (sort + ',') ')' ) sort

       ;

 consts : 'consts' ( mixfixConstDecl + )

        ;

 syntax : 'syntax' (() | mode) ( mixfixConstDecl + );

 mode : '(' name (() | 'output') ')'

      ;

 mixfixConstDecl : constDecl (() | ( '(' mixfix ')' ))

                 ;

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

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

        | ( 'infixr' | 'infixl' ) (() | string) nat

        | 'binder' string nat ;

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

       ;

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

 rules : 'rules' (( id string ) + )

       ;

 defs : 'defs' (( id string ) + )

      ;

 constdefs : 'constdefs' (id '::' (string | type) string +)

           ;

 axclass : 'axclass' classDecl (() | ( id string ) +)

         ;

 instance : 'instance' ( name '<' name | name '::' arity) witness

          ;

 witness : (() | ((string | longident) + ',')) (() | verbatim)

         ;

 oracle : 'oracle' name

        ;

 ml : 'ML' text

    ;

 \end{rail}