# HG changeset patch
# User wenzelm
# Date 1221728243 -7200
# Node ID 91cd65eabd7fb97b4ae24d70d00e7444131f0482
# Parent  2161665a0a5d8f8cb3936fe0b2e5ceecff5d8236
unchecked $ISABELLE_HOME_USER/etc/settings;

diff -r 2161665a0a5d -r 91cd65eabd7f doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Wed Sep 17 23:44:31 2008 +0200
+++ b/doc-src/System/Thy/Basics.thy	Thu Sep 18 10:57:23 2008 +0200
@@ -98,7 +98,7 @@
   of these may have to be adapted (probably @{setting ML_SYSTEM}
   etc.).
   
-  \item The file @{"file" "$ISABELLE_HOME_USER/etc/settings"} (if it
+  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
   exists) is run in the same way as the site default settings. Note
   that the variable @{setting ISABELLE_HOME_USER} has already been set
   before --- usually to @{verbatim "~/isabelle"}.
@@ -166,7 +166,7 @@
   changed in the global setting file.  Typically, the @{setting
   ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
   some extend. In particular, site-wide defaults may be overridden by
-  a private @{"file" "$ISABELLE_HOME_USER/etc/settings"}.
+  a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
   
   \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting
   ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path