src/Doc/System/Basics.thy

   distribution already contains a global settings file with sensible
   defaults for most variables.  When installing the system, only a few
   of these may have to be adapted (probably @{setting ML_SYSTEM}
   etc.).
   
-  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
+  \item The file @{file_unchecked "$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 something like @{verbatim
   "$USER_HOME/.isabelle/IsabelleXXXX"}.
   

   determined from the Isabelle executable that has been invoked.  Do
   not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
   
   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
   counterpart of @{setting ISABELLE_HOME}. The default value is
-  relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
+  relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare
   circumstances this may be 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 @{verbatim
   "$ISABELLE_HOME_USER/etc/settings"}.

   ML system and Isabelle version identifier is appended here, too.
   
   \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
   theory browser information (HTML text, graph data, and printable
   documents) is stored (see also \secref{sec:info}).  The default
-  value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
+  value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
   
   \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
   load if none is given explicitely by the user.  The default value is
   @{verbatim HOL}.
   

   for displaying @{verbatim dvi} files.
   
   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
   prefix from which any running @{executable "isabelle-process"}
   derives an individual directory for temporary files.  The default is
-  somewhere in @{verbatim "/tmp"}.
+  somewhere in @{file_unchecked "/tmp"}.
   
   \end{description}
 *}
 
 

 
   The root of component initialization is @{setting ISABELLE_HOME}
   itself.  After initializing all of its sub-components recursively,
   @{setting ISABELLE_HOME_USER} is included in the same manner (if
   that directory exists).  This allows to install private components
-  via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+  via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
   often more convenient to do that programmatically via the
   \verb,init_component, shell function in the \verb,etc/settings,
   script of \verb,$ISABELLE_HOME_USER, (or any other component
   directory).  For example:
 \begin{ttbox}