doc-src/Ref/theory-syntax.tex
changeset 325 49baeba86546
parent 295 dcde5024895d
child 1080 13c35eb5169b
equal deleted inserted replaced
324:34bc15b546e6 325:49baeba86546
     2 
     2 
     3 \appendix
     3 \appendix
     4 \newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
     4 \newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
     5 
     5 
     6 \chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
     6 \chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
       
     7 Chapter~\ref{sec:ref-defining-theories} explains the meanings of these
       
     8 constructs.  The syntax obeys the following conventions:
     7 \begin{itemize}
     9 \begin{itemize}
     8 \item {\tt Typewriter font} denotes terminal symbols.
    10 \item {\tt Typewriter font} denotes terminal symbols.
     9 \item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
    11 \item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
    10   identifiers, type identifiers, natural numbers, \ML\ strings (with their
    12   identifiers, type identifiers, natural numbers, \ML\ strings (with their
    11   quotation marks) and arbitrary \ML\ text.  The first three are fully defined
    13   quotation marks) and arbitrary \ML\ text.  The first three are fully defined
    12   in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.
    14   in 
       
    15 \iflabelundefined{Defining-Logics}%
       
    16     {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
       
    17     {Chap.\ts\ref{Defining-Logics}}.
    13 \end{itemize}
    18 \end{itemize}
       
    19 Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where
       
    20 {\it text\/} should not contain the character sequence {\tt*)}.
    14 
    21 
    15 \begin{rail}
    22 \begin{rail}
    16 
    23 
    17 theoryDef : id '=' (name + '+') ('+' extension | ());
    24 theoryDef : id '=' (name + '+') ('+' extension | ());
    18 
    25 
    35 sort :  id
    42 sort :  id
    36      | '\{' (id * ',') '\}'
    43      | '\{' (id * ',') '\}'
    37      ;
    44      ;
    38 
    45 
    39 types :  ()
    46 types :  ()
    40       | 'types' ( ( type ( () | '(' infix ')' ) ) + )
    47       | 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + )
    41       ;
    48       ;
    42 
    49 
    43 type : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '='  string );
    50 typeDecl : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '='  string );
    44 
    51 
    45 infix : ( 'infixr' | 'infixl' ) nat;
    52 infix : ( 'infixr' | 'infixl' ) nat;
    46 
    53 
    47 
    54 
    48 arities :  ()
    55 arities :  ()