equal
deleted
inserted
replaced
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 |
7 |
8 Below we present the full syntax of theory definition files as |
8 Below we present the full syntax of theory definition files as provided by |
9 provided by {\Pure} Isabelle --- object-logics may add their own |
9 Pure Isabelle --- object-logics may add their own sections. |
10 sections. \S\ref{sec:ref-defining-theories} explains the meanings of |
10 \S\ref{sec:ref-defining-theories} explains the meanings of these constructs. |
11 these constructs. The syntax obeys the following conventions: |
11 The syntax obeys the following conventions: |
12 \begin{itemize} |
12 \begin{itemize} |
13 \item {\tt Typewriter font} denotes terminal symbols. |
13 \item {\tt Typewriter font} denotes terminal symbols. |
14 |
14 |
15 \item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical |
15 \item $id$, $tid$, $nat$, $string$ and $longident$ are the lexical |
16 classes of identifiers, type identifiers, natural numbers, quoted |
16 classes of identifiers, type identifiers, natural numbers, quoted |