# HG changeset patch
# User wenzelm
# Date 1221728250 -7200
# Node ID bed3865290b49e3ea1150a94eea9419f7025552b
# Parent  91cd65eabd7fb97b4ae24d70d00e7444131f0482
updated generated file;

diff -r 91cd65eabd7f -r bed3865290b4 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Thu Sep 18 10:57:23 2008 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Thu Sep 18 10:57:30 2008 +0200
@@ -116,7 +116,7 @@
   of these may have to be adapted (probably \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}}
   etc.).
   
-  \item The file \hyperlink{file.$ISABELLE-HOME-USER/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER{\isacharslash}etc{\isacharslash}settings}}}} (if it
+  \item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
   exists) is run in the same way as the site default settings. Note
   that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
   before --- usually to \verb|~/isabelle|.
@@ -183,7 +183,7 @@
   \verb|~/isabelle|, under rare circumstances this may be
   changed in the global setting file.  Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to
   some extend. In particular, site-wide defaults may be overridden by
-  a private \hyperlink{file.$ISABELLE-HOME-USER/etc/settings}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER{\isacharslash}etc{\isacharslash}settings}}}}.
+  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
   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