--- a/doc-src/System/Thy/document/Basics.tex Sun Apr 22 22:01:45 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Sun Apr 22 22:02:52 2012 +0200
@@ -167,10 +167,11 @@
\begin{description}
- \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the cross-platform
- user home directory. On Unix systems this is usually the same as
- \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home directory of
- the, not the one of within the Cygwin root file-system.
+ \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the
+ cross-platform user home directory. On Unix systems this is usually
+ the same as \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home
+ directory of the user, not the one of within the Cygwin root
+ file-system.
\item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the location of the
top-level Isabelle distribution directory. This is automatically