# HG changeset patch
# User wenzelm
# Date 1196770975 -3600
# Node ID 6cebd2ff3ab7ad569e24abfd50822505e0c01a9a
# Parent  e123c81257a5aadf0796452571728ddfbd72e863
symbol chi is also a letter;

diff -r e123c81257a5 -r 6cebd2ff3ab7 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Mon Dec 03 17:47:35 2007 +0100
+++ b/doc-src/IsarRef/syntax.tex	Tue Dec 04 13:22:55 2007 +0100
@@ -95,8 +95,8 @@
 greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
       &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
       &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
-      &   & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\
-      &   & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\
+      &   & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
+      &   & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
       &   & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
       &   & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
       &   & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
diff -r e123c81257a5 -r 6cebd2ff3ab7 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Dec 03 17:47:35 2007 +0100
+++ b/src/Pure/General/symbol.ML	Tue Dec 04 13:22:55 2007 +0100
@@ -341,6 +341,7 @@
     ("\\<tau>", Letter),
     ("\\<upsilon>", Letter),
     ("\\<phi>", Letter),
+    ("\\<chi>", Letter),
     ("\\<psi>", Letter),
     ("\\<omega>", Letter),
     ("\\<Gamma>", Letter),