--- a/doc-src/TutorialI/Documents/Documents.thy Thu Mar 25 10:32:21 2004 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Fri Mar 26 05:32:00 2004 +0100
@@ -100,8 +100,8 @@
\end{enumerate}
- Here $ident$ may be any identifier according to the usual Isabelle
- conventions. This results in an infinite store of symbols, whose
+ Here $ident$ is any sequence of letters.
+ This results in an infinite store of symbols, whose
interpretation is left to further front-end tools. For example, the
user-interface of Proof~General + X-Symbol and the Isabelle document
processor (see \S\ref{sec:document-preparation}) display the
@@ -117,6 +117,24 @@
printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
output as @{text "A\<^sup>\<star>"}.
+ A number of symbols are considered letters by the Isabelle lexer
+ and can be used as part of identifiers. These are the greek letters
+ @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}, etc apart from
+ @{text "\<lambda>"}, caligraphic letters like @{text "\<A>"}
+ (\verb+\+\verb+<A>+) and @{text "\<AA>"} (\verb+\+\verb+<AA>+),
+ and the special control symbols \verb+\+\verb+<^isub>+ and
+ \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This
+ means that the input
+
+ \medskip
+ {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,}
+
+ \medskip
+ \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"}
+ by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single entity like
+ @{text "PA"}, not an exponentiation.
+
+
\medskip Replacing our definition of @{text xor} by the following
specifies an Isabelle symbol for the new operator:
*}
--- a/doc-src/TutorialI/Documents/document/Documents.tex Thu Mar 25 10:32:21 2004 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Fri Mar 26 05:32:00 2004 +0100
@@ -104,8 +104,8 @@
\end{enumerate}
- Here $ident$ may be any identifier according to the usual Isabelle
- conventions. This results in an infinite store of symbols, whose
+ Here $ident$ is any sequence of letters.
+ This results in an infinite store of symbols, whose
interpretation is left to further front-end tools. For example, the
user-interface of Proof~General + X-Symbol and the Isabelle document
processor (see \S\ref{sec:document-preparation}) display the
@@ -121,6 +121,24 @@
printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
output as \isa{A\isactrlsup {\isasymstar}}.
+ A number of symbols are considered letters by the Isabelle lexer
+ and can be used as part of identifiers. These are the greek letters
+ \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}, etc apart from
+ \isa{{\isasymlambda}}, caligraphic letters like \isa{{\isasymA}}
+ (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+),
+ and the special control symbols \verb+\+\verb+<^isub>+ and
+ \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This
+ means that the input
+
+ \medskip
+ {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,}
+
+ \medskip
+ \noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}}
+ by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single entity like
+ \isa{PA}, not an exponentiation.
+
+
\medskip Replacing our definition of \isa{xor} by the following
specifies an Isabelle symbol for the new operator:%
\end{isamarkuptext}%