# HG changeset patch
# User kleing
# Date 1080275520 -3600
# Node ID 74c053a2551375e216e4a0a368d86526af02e65a
# Parent  ea2707645af8633f6a09f9be6e5d7592164906ce
symbols in idents

diff -r ea2707645af8 -r 74c053a25513 doc-src/TutorialI/Documents/Documents.thy
--- 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:
 *}
diff -r ea2707645af8 -r 74c053a25513 doc-src/TutorialI/Documents/document/Documents.tex
--- 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}%