diff --git a/lib/Tools/usedir b/lib/Tools/usedir
--- a/lib/Tools/usedir
+++ b/lib/Tools/usedir
@@ -1,254 +1,256 @@
 #!/usr/bin/env bash
 #
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
 #
 # DESCRIPTION: build object-logic or run examples
 
 
 ## diagnostics
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: $PRG [OPTIONS] LOGIC NAME"
   echo
   echo "  Options are:"
   echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
   echo "    -D PATH      dump generated document sources into PATH"
   echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
   echo "    -P PATH      set path for remote theory browsing information"
   echo "    -T LEVEL     multithreading: trace level (default 0)"
   echo "    -V VERSION   declare alternative document VERSION"
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -c BOOL      tell ML system to compress output image (default true)"
   echo "    -d FORMAT    build document as FORMAT (default false)"
   echo "    -f NAME      use ML file NAME (default ROOT.ML)"
   echo "    -g BOOL      generate session graph image for document (default false)"
   echo "    -i BOOL      generate HTML and graph browser information (default false)"
   echo "    -m MODE      add print mode for output"
   echo "    -p LEVEL     set level of detail for proof objects"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
   echo "    -v BOOL      be verbose (default false)"
   echo
   echo "  Build object-logic or run examples. Also creates browsing"
   echo "  information (HTML etc.) according to settings."
   echo
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 function check_bool()
 {
   [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
 }
 
 function check_number()
 {
   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
 }
 
 
 ## process command line
 
 # options
 
 COPY_DUMP=true
 DUMP=""
 MAXTHREADS="1"
 RPATH=""
 TRACETHREADS="0"
 DOCUMENT_VERSIONS=""
 BUILD=""
 COMPRESS=true
 DOCUMENT=false
 ROOT_FILE="ROOT.ML"
 DOCUMENT_GRAPH=false
 INFO=false
 MODES=""
 RESET=false
 SESSION=""
 PROOFS=0
 VERBOSE=false
 
 function getoptions()
 {
   OPTIND=1
   while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
   do
     case "$OPT" in
       C)
         check_bool "$OPTARG"
         COPY_DUMP="$OPTARG"
         ;;
       D)
         DUMP="$OPTARG"
         ;;
       M)
         check_number "$OPTARG"
         MAXTHREADS="$OPTARG"
         ;;
       P)
         RPATH="$OPTARG"
         ;;
       T)
         check_number "$OPTARG"
         TRACETHREADS="$OPTARG"
         ;;
       V)
         if [ -z "$DOCUMENT_VERSIONS" ]; then
           DOCUMENT_VERSIONS="\"$OPTARG\""
         else
           DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\""
         fi
         ;;
       b)
         BUILD=true
         ;;
       c)
         check_bool "$OPTARG"
         COMPRESS="$OPTARG"
         ;;
       d)
         DOCUMENT="$OPTARG"
         ;;
       f)
         ROOT_FILE="$OPTARG"
         ;;
       g)
         check_bool "$OPTARG"
         DOCUMENT_GRAPH="$OPTARG"
         ;;
       i)
         check_bool "$OPTARG"
         INFO="$OPTARG"
         ;;
       m)
         if [ -z "$MODES" ]; then
           MODES="\"$OPTARG\""
         else
           MODES="\"$OPTARG\", $MODES"
         fi
         ;;
       p)
         check_number "$OPTARG"
         PROOFS="$OPTARG"
         ;;
       r)
         RESET=true
         ;;
       s)
         SESSION="$OPTARG"
         ;;
       v)
         check_bool "$OPTARG"
         VERBOSE="$OPTARG"
         ;;
       \?)
         usage
         ;;
     esac
   done
 }
 
 getoptions $ISABELLE_USEDIR_OPTIONS
 
 getoptions "$@"
 shift $(($OPTIND - 1))
 
 
 # args
 
 [ "$#" -ne 2 ] && usage
 
 LOGIC="$1"; shift
 NAME="$1"; shift
 
 [ -z "$SESSION" ] && SESSION=$(basename "$NAME")
 
 
 
 ## main
 
 # prepare browser info dir
 
-if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
+if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/library_index_header.html" ]; then
   mkdir -p "$ISABELLE_BROWSER_INFO"
   cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
-  cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
+  cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
+    "$ISABELLE_HOME/lib/html/library_index_content.template" \
+    "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
 fi
 
 
 # prepare log dir
 
 LOGDIR="$ISABELLE_OUTPUT/log"
 mkdir -p "$LOGDIR"
 
 
 # run isabelle
 
 PARENT=$(basename "$LOGIC")
 
 if [ -z "$BUILD" ]; then
   cd "$NAME" || fail "Bad session directory '$NAME'"
 fi
 
 if [ "$DOCUMENT" != false ]; then
   DOC="$DOCUMENT"
 else
   DOC=""
 fi
 
 
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 if [ -n "$BUILD" ]; then
   ITEM="$SESSION"
   echo "Building $ITEM ..." >&2
   LOG="$LOGDIR/$ITEM"
 
   OPT_C=""
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE" \
     -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS;" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
   ITEM=$(basename "$LOGIC")-"$SESSION"
   echo "Running $ITEM ..." >&2
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \
     -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
 fi
 
 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
 
 
 # exit status
 
 if [ "$RC" -eq 0 ]; then
   echo "Finished $ITEM ($TIMES_REPORT)" >&2
   gzip --force "$LOG"
 else
   { echo "$ITEM FAILED";
     echo "(see also $LOG)";
     echo; tail "$LOG"; echo; } >&2
 fi
 
 exit "$RC"