
diff -r 3003be923908 -r ffcff7509a49 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Tue Nov 16 20:30:25 2010 +0100
+++ b/doc-src/System/Thy/Basics.thy	Tue Nov 16 21:48:14 2010 +0100
@@ -309,12 +309,18 @@
   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).  Thus users can easily add private
-  components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
-
-  It is also possible to initialize components programmatically via
-  the \verb,init_component, shell function, say within the
-  \verb,settings, script of another component.
+  that directory exists).  This allows to install private components
+  via @{verbatim "$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{verbatim}
+  if [ -d "$HOME/screwdriver-2.0" ]
+  then
+    init_component "$HOME/screwdriver-2.0"
+  else
+  \end{verbatim}
 *}
 
 




