equal
deleted
inserted
replaced
15 \emph{atomic entities} within outer syntax. For example, the string |
15 \emph{atomic entities} within outer syntax. For example, the string |
16 \texttt{"x + y"} and identifier \texttt{z} are legal term specifications |
16 \texttt{"x + y"} and identifier \texttt{z} are legal term specifications |
17 within a theory, while \texttt{x + y} is not. |
17 within a theory, while \texttt{x + y} is not. |
18 |
18 |
19 \begin{warn} |
19 \begin{warn} |
20 Note that classic Isabelle theories used to fake parts of the inner type |
20 Note that classic Isabelle theories used to fake parts of the inner syntax |
21 syntax, with rather complicated rules when quotes may be omitted. Despite |
21 of types, with rather complicated rules when quotes may be omitted. Despite |
22 the minor drawback of requiring quotes more often, the syntax of |
22 the minor drawback of requiring quotes more often, the syntax of |
23 Isabelle/Isar is simpler and more robust in that respect. |
23 Isabelle/Isar is simpler and more robust in that respect. |
24 \end{warn} |
24 \end{warn} |
25 |
25 |
26 \medskip |
26 \medskip |
67 a backslash. Note that ML-style control characters are \emph{not} supported. |
67 a backslash. Note that ML-style control characters are \emph{not} supported. |
68 The body of \texttt{verbatim} may consist of any text not containing |
68 The body of \texttt{verbatim} may consist of any text not containing |
69 ``\verb|*}|''. |
69 ``\verb|*}|''. |
70 |
70 |
71 Comments take the form \texttt{(*~\dots~*)} and may be |
71 Comments take the form \texttt{(*~\dots~*)} and may be |
72 nested\footnote{Proof~General may get confused by nested comments.}, just as |
72 nested\footnote{Proof~General may occasionally get confused by nested |
73 in ML. Note that these are \emph{source} comments only, which are stripped |
73 comments.}, just as in ML. Note that these are \emph{source} comments only, |
74 after lexical analysis of the input. The Isar document syntax also provides |
74 which are stripped after lexical analysis of the input. The Isar document |
75 \emph{formal comments} that are actually part of the text (see |
75 syntax also provides \emph{formal comments} that are actually part of the text |
76 \S\ref{sec:comments}). |
76 (see \S\ref{sec:comments}). |
77 |
77 |
78 |
78 |
79 \section{Common syntax entities} |
79 \section{Common syntax entities} |
80 |
80 |
81 Subsequently, we introduce several basic syntactic entities, such as names, |
81 Subsequently, we introduce several basic syntactic entities, such as names, |