diff -r 6b0e3e4e1891 -r a30b7169fdd1 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Sat Oct 04 16:19:00 2008 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Sat Oct 04 16:19:49 2008 +0200
@@ -143,7 +143,7 @@
 
   \begin{itemize}
 
-  \item \indexdef{}{setting}{ISABELLE}\hypertarget{setting.ISABELLE}{\hyperlink{setting.ISABELLE}{\mbox{\isa{\isatt{ISABELLE}}}}} and \indexdef{}{setting}{ISATOOL}\hypertarget{setting.ISATOOL}{\hyperlink{setting.ISATOOL}{\mbox{\isa{\isatt{ISATOOL}}}}} are set
+  \item \indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}} and \indexdef{}{setting}{ISABELLE\_TOOL}\hypertarget{setting.ISABELLE-TOOL}{\hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}} are set
   automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables,
   respectively.
   
@@ -185,7 +185,7 @@
   some extend. In particular, site-wide defaults may be overridden by
   a private \verb|$ISABELLE_HOME_USER/etc/settings|.
   
-  \item[\indexdef{}{setting}{ISABELLE}\hypertarget{setting.ISABELLE}{\hyperlink{setting.ISABELLE}{\mbox{\isa{\isatt{ISABELLE}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISATOOL}{\mbox{\isa{\isatt{ISATOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
+  \item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
   names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables, respectively.  Thus other tools and scripts
   need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
   on the current search path of the shell.