# HG changeset patch
# User kleing
# Date 1080193479 -3600
# Node ID 6eac487f9cfa7ed0c2d333284c17b9ca6a6d5763
# Parent  82774ac788aef076dbdef2114928f04fb1c2f87a
documented new identifier syntax

diff -r 82774ac788ae -r 6eac487f9cfa doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Thu Mar 25 05:37:32 2004 +0100
+++ b/doc-src/IsarRef/syntax.tex	Thu Mar 25 06:44:39 2004 +0100
@@ -79,17 +79,28 @@
   typefree & = & \verb,',ident \\
   typevar & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
   string & = & \verb,", ~\dots~ \verb,", \\
-  verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\
-\end{matharray}
-\begin{matharray}{rcl}
-  letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
+  verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex]
+
+  letter & = & sletter ~|~ xletter \\
   digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
   quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
   sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
    \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
   & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
   \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
-  symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots
+  symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots\\
+sletter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
+xletter & = & {\tt \backslash<} ~ (sletter ~|~ dletter ~|~ gletter ~|~ cletter) ~ {\tt >}\\
+dletter & = & \verb,aa, ~|~ \dots ~|~ \verb,zz, ~|~ \verb,AA, ~|~ \dots ~|~ \verb,ZZ, \\
+bletter & = & {\tt bool} ~|~ {\tt complex} ~|~ {\tt nat} ~|~ {\tt rat} ~|~ {\tt real} ~|~ {\tt int}\\
+cletter & = & {\tt \hat{}\, isup} ~~|~~ {\tt \hat{}\, isub}
+\end{matharray}
+\begin{matharray}{rcl}
+gletter & = & {\tt alpha} ~|~ {\tt beta} ~|~ {\tt gamma} ~|~ {\tt delta} ~|~ {\tt epsilon} ~|~ {\tt zeta} ~|~ {\tt eta} ~|\\ 
+        &   & {\tt theta} ~|~ {\tt iota} ~|~ {\tt kappa} ~|~ {\tt mu} ~|~ {\tt nu} ~|~ {\tt xi} ~|~ {\tt pi} ~|~ {\tt rho} ~|\\
+        &   & {\tt sigma} ~|~ {\tt tau} ~|~ {\tt upsilon} ~|~ {\tt phi} ~|~ {\tt psi} ~|~ {\tt omega} ~|~ {\tt Gamma} ~|\\
+        &   & {\tt Delta} ~|~ {\tt Theta} ~|~ {\tt Lambda} ~|~ {\tt Xi} ~|~ {\tt Pi} ~|~ {\tt Sigma} ~|~ {\tt Upsilon} ~|\\
+        &   & {\tt Phi} ~|~ {\tt Psi} ~|~ {\tt Omega}
 \end{matharray}
 
 The syntax of $string$ admits any characters, including newlines; ``\verb|"|''
@@ -117,6 +128,12 @@
 Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as
 ``\verb,\<forall>,''.  Concerning Isabelle itself, any sequence of the form
 \verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol.
+Greek letters \verb+\<alpha>+, \verb+\<beta>+, etc (apart from
+\verb+\<lambda>+), caligraphic letters in various styles, as
+well as the special \verb+\<^isub>+ and \verb+\<^isup>+ sub/superscipt
+control characters are considered proper letters and can be used as
+part of any identifier. 
+
 Display of appropriate glyphs is a matter of front-end tools, say the
 user-interface of Proof~General plus the X-Symbol package, or the {\LaTeX}
 macro setup of document output.  A list of predefined Isabelle symbols is
diff -r 82774ac788ae -r 6eac487f9cfa doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Thu Mar 25 05:37:32 2004 +0100
+++ b/doc-src/Ref/defining.tex	Thu Mar 25 06:44:39 2004 +0100
@@ -239,10 +239,20 @@
                   \mbox{\tt ?}tid\mbox{\tt .}nat \\
 xnum      & =   & \mbox{\tt \#}nat ~~|~~ \mbox{\tt \#-}nat \\
 xstr      & =   & \mbox{\tt ''\rm text\tt ''} \\[1ex]
-letter    & =   & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
+letter    & =   & sletter ~~|~~ xletter \\
 digit     & =   & \mbox{one of {\tt 0}\dots {\tt 9}} \\
 quasiletter & =  & letter ~~|~~ digit ~~|~~ \mbox{\tt _} ~~|~~ \mbox{\tt '} \\
-nat       & =   & digit^+
+nat       & =   & digit^+\\[1ex]
+sletter & = & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
+xletter & = & {\tt \backslash<} ~ (sletter ~|~ dletter ~|~ gletter ~|~ cletter) ~ {\tt >}\\
+dletter & = & \mbox{one of {\tt aa}\dots {\tt zz} {\tt AA}\dots {\tt ZZ}} \\
+bletter & = & {\tt bool} ~|~ {\tt complex} ~|~ {\tt nat} ~|~ {\tt rat} ~|~ {\tt real} ~|~ {\tt int}\\
+gletter & = & {\tt alpha} ~|~ {\tt beta} ~|~ {\tt gamma} ~|~ {\tt delta} ~|~ {\tt epsilon} ~|~ {\tt zeta} ~|~ {\tt eta} ~|\\ 
+        &   & {\tt theta} ~|~ {\tt iota} ~|~ {\tt kappa} ~|~ {\tt mu} ~|~ {\tt nu} ~|~ {\tt xi} ~|~ {\tt pi} ~|~ {\tt rho} ~|\\
+        &   & {\tt sigma} ~|~ {\tt tau} ~|~ {\tt upsilon} ~|~ {\tt phi} ~|~ {\tt psi} ~|~ {\tt omega} ~|~ {\tt Gamma} ~|\\
+        &   & {\tt Delta} ~|~ {\tt Theta} ~|~ {\tt Lambda} ~|~ {\tt Xi} ~|~ {\tt Pi} ~|~ {\tt Sigma} ~|~ {\tt Upsilon} ~|\\
+        &   & {\tt Phi} ~|~ {\tt Psi} ~|~ {\tt Omega}\\
+cletter & = & {\tt \hat{}\, isup} ~~|~~ {\tt \hat{}\, isub}
 \end{eqnarray*}
 The lexer repeatedly takes the longest prefix of the input string that
 forms a valid token.  A maximal prefix that is both a delimiter and a