diff --git a/etc/settings b/etc/settings
--- a/etc/settings
+++ b/etc/settings
@@ -1,212 +1,214 @@
 # -*- shell-script -*- :mode=shellscript:
 #
 # Isabelle settings -- distribution defaults.
 #
 # Important notes:
 #   * See the "system" manual for explanations on Isabelle settings
 #   * DO NOT EDIT the repository copy of this file!
 #   * DO NOT COPY this file into your ~/.isabelle directory!
 
 ###
 ### ML compiler settings (ESSENTIAL!)
 ###
 
 # ML_HOME specifies the location of the actual compiler binaries.  Do
 # not invent new ML system names unless you know what you are doing.
 # Only one of the sections below should be activated.
 
 # Poly/ML default (automated settings)
 ML_PLATFORM="$ISABELLE_PLATFORM"
 ML_HOME="$(choosefrom \
   "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
   "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
   "/usr/local/polyml/$ML_PLATFORM" \
   "/usr/share/polyml/$ML_PLATFORM" \
   "/opt/polyml/$ML_PLATFORM" \
   "")"
 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
 ML_OPTIONS="-H 200"
 ML_SOURCES="$ML_HOME/../src"
 
 # Poly/ML 32 bit (manual settings)
 #ML_SYSTEM=polyml-5.4.1
 #ML_PLATFORM="$ISABELLE_PLATFORM"
 #ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
 #ML_OPTIONS="-H 500"
 #ML_SOURCES="$ML_HOME/../src"
 
 # Poly/ML 64 bit (manual settings)
 #ML_SYSTEM=polyml-5.4.1
 #ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
 #ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
 #ML_OPTIONS="-H 1000"
 #ML_SOURCES="$ML_HOME/../src"
 
 # Standard ML of New Jersey (slow!)
 #ML_SYSTEM=smlnj-110
 #ML_HOME="/usr/local/smlnj/bin"
 #ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 #SMLNJ_CYGWIN_RUNTIME=1
 
 
 ###
 ### JVM components (Scala or Java)
 ###
 
 ISABELLE_SCALA_BUILD_OPTIONS="-nowarn -target:jvm-1.5"
 
 
 ###
 ### Interactive sessions (cf. isabelle tty)
 ###
 
 ISABELLE_LINE_EDITOR=""
 [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
 [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
 
 
 ###
 ### Batch sessions
 ###
 
 #cf. isabelle usedir
 ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML"
 
 #cf. isabelle build
 ISABELLE_BUILD_OPTIONS=""
 
 
 ###
 ### Document preparation (cf. isabelle latex/document)
 ###
 
 ISABELLE_LATEX="latex"
 ISABELLE_PDFLATEX="pdflatex"
 ISABELLE_BIBTEX="bibtex"
 ISABELLE_MAKEINDEX="makeindex"
 ISABELLE_DVIPS="dvips -D 600"
 ISABELLE_EPSTOPDF="epstopdf"
 
 # Paranoia setting for strange latex installations ...
 #unset TEXMF
 
 
 ###
 ### Misc path settings
 ###
 
+ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
+
 # The place for user configuration, heap files, etc.
 if [ -z "$ISABELLE_IDENTIFIER" ]; then
   ISABELLE_HOME_USER="$USER_HOME/.isabelle"
 else
   ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
 fi
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
 
 # Location for temporary files (should be on a local file system).
 ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
 
 # Heap input locations. ML system identifier is included in lookup.
 ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
 
 # Heap output location. ML system identifier is appended automatically later on.
 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
   { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
 ISABELLE_SITE_SETTINGS_PRESENT=true
 
 
 ###
 ### Default logic
 ###
 
 ISABELLE_LOGIC=HOL
 
 
 ###
 ### Docs
 ###
 
 # Where to look for docs (multiple dirs separated by ':').
 ISABELLE_DOCS="$ISABELLE_HOME/doc"
 
 # Preferred document format
 ISABELLE_DOC_FORMAT=pdf
 
 # The dvi file viewer
 DVI_VIEWER=xdvi
 #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
 #DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7"
 #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
 #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
 
 # The pdf file viewer
 case "$ISABELLE_PLATFORM" in
   *-linux)
     PDF_VIEWER="xdg-open"
     ;;
   *-darwin)
     PDF_VIEWER="open -W -n"
     ;;
   *-cygwin)
     PDF_VIEWER="cygstart"
     ;;
 esac
 
 
 # Printer spool command for PS files
 PRINT_COMMAND=lp
 
 
 ###
 ### Rendering information
 ###
 
 ISABELLE_FONTS="$ISABELLE_HOME/lib/fonts/IsabelleText.ttf:$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
 
 
 ###
 ### Old-style settings for some external tools
 ###
 
 ## Set HOME only for tools you have installed!
 
 # SVC (Stanford Validity Checker)
 #SVC_HOME=
 #SVC_MACHINE=i386-redhat-linux
 #SVC_MACHINE=sparc-sun-solaris
 
 # MiniSat 1.14 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
 #MINISAT_HOME=/usr/local/bin
 
 # zChaff (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
 #ZCHAFF_HOME=/usr/local/bin
 
 # BerkMin561 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
 #BERKMIN_HOME=/usr/local/bin
 #BERKMIN_EXE=BerkMin561-linux
 #BERKMIN_EXE=BerkMin561-solaris
 
 # Jerusat 1.3 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
 #JERUSAT_HOME=/usr/local/bin
 
 # For configuring HOL/Matrix/cplex
 # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
 # First option: use the commercial cplex solver
 #LP_SOLVER=CPLEX
 #CPLEX_PATH=cplex
 # Second option: use the open source glpk solver
 #LP_SOLVER=GLPK
 #GLPK_PATH=glpsol
 
 # Misc programming languages
 #ISABELLE_GHC="/usr/bin/ghc"
 #ISABELLE_OCAML="/usr/bin/ocaml"
 #ISABELLE_SWIPL="/usr/bin/swipl"
diff --git a/lib/Tools/components b/lib/Tools/components
new file mode 100755
--- /dev/null
+++ b/lib/Tools/components
@@ -0,0 +1,120 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: resolve Isabelle components
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
+  echo
+  echo "  Options are:"
+  echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
+  echo "    -a           all missing components"
+  echo "    -l           list status"
+  echo
+  echo "  Resolve Isabelle components via download and installation."
+  echo "  COMPONENTS are identified via base name."
+  echo
+  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+#options
+
+COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
+ALL_MISSING=""
+LIST_ONLY=""
+
+while getopts "R:al" OPT
+do
+  case "$OPT" in
+    R)
+      COMPONENT_REPOSITORY="$OPTARG"
+      ;;
+    a)
+      ALL_MISSING="true"
+      ;;
+    l)
+      LIST_ONLY="true"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -eq 0 -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
+
+if [ -z "$ALL_MISSING" ]; then
+  splitarray ":" "$@"
+else
+  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
+fi
+declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
+
+
+## main
+
+splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
+splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
+
+if [ -n "$LIST_ONLY" ]; then
+  echo
+  echo "Available components:"
+  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
+  echo
+  echo "Missing components:"
+  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
+else
+  for NAME in "${SELECTED_COMPONENTS[@]}"
+  do
+    BASE_NAME="$(basename "$NAME")"
+    FULL_NAME=""
+    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
+    do
+      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
+    done
+    if [ -z "$FULL_NAME" ]; then
+      echo "Ignoring irrelevant component \"$NAME\""
+    elif [ -d "$FULL_NAME" ]; then
+      echo "Skipping existing component \"$FULL_NAME\""
+    else
+      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
+        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
+        echo "Getting \"$REMOTE\""
+        perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
+        if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
+        then
+          rm -f "${FULL_NAME}.tar.gz"
+        fi
+      fi
+      if [ -e "${FULL_NAME}.tar.gz" ]; then
+        echo "Unpacking \"${FULL_NAME}.tar.gz\""
+        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz"
+      fi
+    fi
+  done
+fi
+