8 constructs. The syntax obeys the following conventions: |
8 constructs. The syntax obeys the following conventions: |
9 \begin{itemize} |
9 \begin{itemize} |
10 \item {\tt Typewriter font} denotes terminal symbols. |
10 \item {\tt Typewriter font} denotes terminal symbols. |
11 \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 |
12 identifiers, type identifiers, natural numbers, \ML\ strings (with their |
12 identifiers, type identifiers, natural numbers, \ML\ strings (with their |
13 quotation marks) and arbitrary \ML\ text. The first three are fully defined |
13 quotation marks, but without the need for \verb$\$ at the end of a line and |
14 in |
14 the beginning of the next line) and arbitrary \ML\ text. The first three |
15 \iflabelundefined{Defining-Logics}% |
15 are fully defined in \iflabelundefined{Defining-Logics}% |
16 {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}% |
16 {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}% |
17 {Chap.\ts\ref{Defining-Logics}}. |
17 {Chap.\ts\ref{Defining-Logics}}. |
18 \end{itemize} |
18 \end{itemize} |
19 Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where |
19 Comments in theories take the form {\tt (*} {\it text\/} {\tt*)}, where |
20 {\it text\/} should not contain the character sequence {\tt*)}. |
20 {\it text\/} should not contain the character sequence {\tt*)}. |