1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Ref/theory-syntax.tex	Mon Mar 21 10:51:28 1994 +0100
     1.3 @@ -0,0 +1,83 @@
     1.4 +%% $Id$
     1.5 +
     1.6 +\appendix
     1.7 +\newlinechar=-1  %mathsing.sty sets \newlinechar=`\|, which would cause mayhem
     1.8 +
     1.9 +\chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
    1.10 +\begin{itemize}
    1.11 +\item {\tt Typewriter font} denotes terminal symbols.
    1.12 +\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
    1.13 +  identifiers, type identifiers, natural numbers, \ML\ strings (with their
    1.14 +  quotation marks) and arbitrary \ML\ text.  The first three are fully defined
    1.15 +  in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.
    1.16 +\end{itemize}
    1.17 +
    1.18 +\begin{rail}
    1.19 +
    1.20 +theoryDef : id '=' (name + '+') ('+' extension | ());
    1.21 +
    1.22 +name: id | string;
    1.23 +
    1.24 +extension : classes default types arities consts trans rules 'end' ml
    1.25 +          ;
    1.26 +
    1.27 +classes : ()
    1.28 +        | 'classes' ( ( id (  ()
    1.29 +                            | '<' (id + ',')
    1.30 +                           ) 
    1.31 +                       ) + )
    1.32 +        ;
    1.33 +
    1.34 +default : ()
    1.35 +        | 'default' sort 
    1.36 +        ;
    1.37 +
    1.38 +sort :  id
    1.39 +     | '\{' (id * ',') '\}'
    1.40 +     ;
    1.41 +
    1.42 +types :  ()
    1.43 +      | 'types' ( ( type ( () | '(' infix ')' ) ) + )
    1.44 +      ;
    1.45 +
    1.46 +type : ( () | tid | '(' ( tid + ',' ) ')') name ( () | '='  string );
    1.47 +
    1.48 +infix : ( 'infixr' | 'infixl' ) nat;
    1.49 +
    1.50 +
    1.51 +arities :  ()
    1.52 +        | 'arities' ((( name + ',' ) '::' arity ) + )
    1.53 +        ;
    1.54 +
    1.55 +arity   : ( () 
    1.56 +          | '(' (sort + ',') ')' 
    1.57 +          ) id
    1.58 +        ;
    1.59 +
    1.60 +
    1.61 +consts :  ()
    1.62 +       | 'consts' ( ( constDecl ( () | ( '(' mixfix ')' ) ) ) + )
    1.63 +       ;
    1.64 +
    1.65 +constDecl : ( name + ',') '::' string ;
    1.66 +
    1.67 +
    1.68 +mixfix :  string ( () | ( () | ('[' (nat + ',') ']')) nat )
    1.69 +       | infix
    1.70 +       | 'binder' string nat ;
    1.71 +
    1.72 +trans : ()
    1.73 +      | 'translations' ( pat ( '==' | '=>' | '<=' ) pat + )
    1.74 +      ;
    1.75 +
    1.76 +pat : ( () | ( '(' id ')' ) ) string;
    1.77 +
    1.78 +rules :  ()
    1.79 +      | 'rules' (( id string ) + )
    1.80 +      ;
    1.81 +
    1.82 +ml :  ()
    1.83 +   | 'ML' text
    1.84 +   ;
    1.85 +
    1.86 +\end{rail}