# HG changeset patch
# User noschinl
# Date 1357907056 -3600
# Node ID e8d641235191aa868ca9afc8650f7390a82f02b3
# Parent  5601ae5926791ae16f22cb6a454c939dc0e78185# Parent  5d4852f1b952aff0729bc5a0ca04e414cdac6059
merged

diff -r 5601ae592679 -r e8d641235191 Admin/MacOS/App1/build
--- a/Admin/MacOS/App1/build	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/MacOS/App1/build	Fri Jan 11 13:24:16 2013 +0100
@@ -18,3 +18,6 @@
   -f "$COCOADIALOG_APP" \
   "$THIS/script" \
   "$PWD/Isabelle.app"
+
+rm -f Contents/Resources/Isabelle
+ln -s Contents/Resources/Isabelle Isabelle.app/Isabelle
\ No newline at end of file
diff -r 5601ae592679 -r e8d641235191 Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/MacOS/App1/script	Fri Jan 11 13:24:16 2013 +0100
@@ -9,7 +9,13 @@
 SUPER_APP="$(cd "$THIS/../../.."; pwd)"
 
 
-# sane environment defaults
+# global defaults
+
+ISABELLE_TOOL="$THIS/Isabelle/bin/isabelle"
+PROOFGENERAL_EMACS="$THIS/Aquamacs.app/Contents/MacOS/Aquamacs"
+
+
+# environment
 
 cd "$HOME"
 if [ -x /usr/libexec/path_helper ]; then
@@ -19,46 +25,6 @@
 [ -z "$LANG" ] && export LANG=en_US.UTF-8
 
 
-# settings support
-
-function choosefrom ()
-{
-  local RESULT=""
-  local FILE=""
-
-  for FILE in "$@"
-  do
-    [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE"
-  done
-
-  [ -z "$RESULT" ] && RESULT="$FILE"
-  echo "$RESULT"
-}
-
-
-# Isabelle
-
-ISABELLE_TOOL="$(choosefrom \
-  "$THIS/Isabelle/bin/isabelle" \
-  "$SUPER_APP/Isabelle/bin/isabelle" \
-  "$HOME/bin/isabelle" \
-  isabelle)"
-
-
-# Proof General / Emacs
-
-PROOFGENERAL_EMACS="$(choosefrom \
-  "$THIS/Aquamacs.app/Contents/MacOS/Aquamacs" \
-  "$SUPER_APP/Aquamacs.app/Contents/MacOS/Aquamacs" \
-  /Applications/Aquamacs.app/Contents/MacOS/Aquamacs \
-  "")"
-
-declare -a EMACS_OPTIONS=()
-if [ -n "$PROOFGENERAL_EMACS" ]; then
-  EMACS_OPTIONS=(-p "$PROOFGENERAL_EMACS")
-fi
-
-
 # run interface with error feedback
 
 ISABELLE_INTERFACE_CHOICE="$("$ISABELLE_TOOL" getenv -b ISABELLE_INTERFACE_CHOICE)"
@@ -68,12 +34,12 @@
   CHOICE=($("$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" dropdown \
     --title Isabelle \
     --text "Which Isabelle interface?" \
-    --items "Emacs / Proof General" "Isabelle/jEdit PIDE" \
+    --items "Isabelle/jEdit PIDE" "Emacs / Proof General" \
     --button2 "OK, do not ask again" --button1 "OK"))
   if [ "${CHOICE[1]}" = 0 ]; then
-    ISABELLE_INTERFACE_CHOICE=emacs
+    ISABELLE_INTERFACE_CHOICE=jedit
   else
-    ISABELLE_INTERFACE_CHOICE=jedit
+    ISABELLE_INTERFACE_CHOICE=emacs
   fi
   if [ "${CHOICE[0]}" = 2 ]; then
     ISABELLE_HOME_USER="$("$ISABELLE_TOOL" getenv -b ISABELLE_HOME_USER)"
@@ -91,10 +57,10 @@
 OUTPUT="/tmp/isabelle$$.out"
 
 if [ "$ISABELLE_INTERFACE_CHOICE" = emacs ]; then
-  ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
+  ( "$ISABELLE_TOOL" emacs -p "$PROOFGENERAL_EMACS" "$@" ) > "$OUTPUT" 2>&1
   RC=$?
 else
-  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
+  ( "$ISABELLE_TOOL" jedit -s "$@" ) > "$OUTPUT" 2>&1
   RC=$?
 fi
 
diff -r 5601ae592679 -r e8d641235191 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Release/CHECKLIST	Fri Jan 11 13:24:16 2013 +0100
@@ -7,6 +7,8 @@
 
 - test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
 
+- test scala-2.9.2;
+
 - test Proof General 4.1, 3.7.1.1;
 
 - check HTML header of library;
@@ -53,9 +55,7 @@
 
 - hg up -r DISTNAME && isabelle makedist -r DISTNAME;
 
-- makebin (multiplatform);
-
-- makebundle (multiplatform);
+- isabelle makedist_bundles;
 
 - Mac OS X: hdiutil create -srcfolder DIR DMG;
 
@@ -67,8 +67,6 @@
 Final release stage
 ===================
 
-- makedist: REPOS_NAME="isabelle-release"
-
 - various .hg/hgrc files:
   default = /home/isabelle-repository/repos/isabelle-release
 
diff -r 5601ae592679 -r e8d641235191 Admin/Release/makebundle
--- a/Admin/Release/makebundle	Thu Jan 10 21:22:11 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-#!/usr/bin/env bash
-#
-# makebundle -- re-package with add-on components
-
-## diagnostics
-
-PRG=$(basename "$0")
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG ARCHIVE PLATFORM"
-  echo
-  echo "  Re-package Isabelle source distribution with add-on components"
-  echo "  and heap images"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## implicit and explicit arguments
-
-TMP="/var/tmp/isabelle-makebundle$$"
-mkdir "$TMP" || fail "Cannot create directory $TMP"
-
-[ "$#" -ne 2 ] && usage
-
-ARCHIVE="$1"; shift
-PLATFORM="$1"; shift
-
-[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
-
-
-## main
-
-ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
-ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
-ISABELLE_HOME="$TMP/$ISABELLE_NAME"
-
-tar -C "$TMP" -x -z -f "$ARCHIVE"
-
-
-echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
-
-for CONTRIB in "$ARCHIVE_DIR/contrib/"*.tar.gz "$ARCHIVE_DIR/contrib/$PLATFORM"/*.tar.gz
-do
-  if [ -f "$CONTRIB" ]; then
-    tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB"
-    NAME="$(basename "$CONTRIB" .tar.gz)"
-    [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB"
-
-    if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
-      echo "component $NAME"
-      if [ "$PLATFORM" != x86-cygwin -a "$NAME" = ProofGeneral-3.7.1.1 ]; then
-        echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
-      elif [ "$PLATFORM" = x86-cygwin -a "$NAME" = ProofGeneral-4.1 ]; then
-        echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
-      else
-        echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
-      fi
-    else
-      echo "package $NAME"
-    fi
-  fi
-done
-
-if [ "$PLATFORM" = x86-cygwin ]; then
-  TAR="$ARCHIVE_DIR/contrib/x86-cygwin/Isabelle.tar"
-  [ -e "$TAR" ] || fail "Missing $TAR"
-  rm -f "$ISABELLE_HOME/Isabelle"
-  tar -C "$ISABELLE_HOME" -xv -f "$TAR"
-
-  (
-    cd "$ISABELLE_HOME"
-    for DIR in $(find contrib -name x86-linux -o -name x86_64-linux -o -name x86-darwin -o -name x86_64-darwin | sort)
-    do
-      echo "removing $DIR"
-      rm -rf "$DIR"
-    done
-  )
-
-  mv "$ISABELLE_HOME/contrib"/polyml* "$ISABELLE_HOME/contrib/cygwin-1.7.9/usr/local/"
-  (
-    cd "$ISABELLE_HOME/contrib/cygwin-1.7.9"
-    find usr/local/polyml-*/x86-cygwin | gzip > etc/setup/polyml.lst.gz
-  )
-
-  for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
-  do
-    FILE="$ISABELLE_HOME/$NAME"
-    {
-      echo '<?xml version="1.0" encoding="utf-8" ?>'
-      echo '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'
-      echo '<html xmlns="http://www.w3.org/1999/xhtml">'
-      echo '<head>'
-      echo '<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>'
-      echo "<title>${NAME}</title>"
-      echo '</head>'
-      echo '<body>'
-      echo '<pre>'
-      perl -w -p -e "s/&/&amp;/g; s/</&lt;/g; s/>/&gt;/g; s/'/&apos;/g; s/\"/&quot;/g;" "$FILE"
-      echo '</pre>'
-      echo '</body>'
-    } > "${FILE}.html"
-  done
-fi
-
-
-HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz"
-[ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE"
-echo "heaps"
-tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE"
-
-case "$PLATFORM" in
-  x86_64-linux)
-    perl -pi -e 's,^ML_PLATFORM=.*$,ML_PLATFORM="\$ISABELLE_PLATFORM64",g;' "$TMP/$ISABELLE_NAME/etc/settings"
-    perl -pi -e "s,^ML_OPTIONS=.*$,ML_OPTIONS=\"-H 400\",g;" "$TMP/$ISABELLE_NAME/etc/settings"
-    ;;
-  *-darwin)
-    perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
-      -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
-      -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
-      "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
-    ;;
-  *-cygwin)
-    perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
-      "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
-    ;;
-  *)
-    ;;
-esac
-
-BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
-
-echo "$(basename "$BUNDLE_ARCHIVE")"
-tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME"
-
-
-# clean up
-cd /tmp
-rm -rf "$TMP"
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/Cygwin/Cygwin-Setup.bat
--- a/Admin/Windows/Cygwin/Cygwin-Setup.bat	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat	Fri Jan 11 13:24:16 2013 +0100
@@ -1,4 +1,4 @@
 @echo off
 
-"%CD%\contrib\cygwin-1.7.9\setup" --site http://isabelle.in.tum.de/cygwin --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin-1.7.9"
+"%CD%\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\cygwin"
 
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/Cygwin/Cygwin-Terminal.bat
--- a/Admin/Windows/Cygwin/Cygwin-Terminal.bat	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/Cygwin/Cygwin-Terminal.bat	Fri Jan 11 13:24:16 2013 +0100
@@ -6,4 +6,4 @@
 
 echo This is the GNU Bash interpreter of Cygwin.
 echo Use command "isabelle" to invoke Isabelle tools.
-"%CD%\contrib\cygwin-1.7.9\bin\bash" --login -i
+"%CD%\cygwin\bin\bash" --login -i
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/Cygwin/init.bat
--- a/Admin/Windows/Cygwin/init.bat	Thu Jan 10 21:22:11 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-@echo off
-
-cd "%~dp0"
-cd "..\.."
-
-echo Initializing ...
-"contrib\cygwin-1.7.9\bin\ash" /bin/rebaseall
-"contrib\cygwin-1.7.9\bin\bash" -c "PATH=/bin; chmod -wx $(find heaps -type f); mkpasswd -l >/etc/passwd; mkgroup -l >/etc/group"
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/Cygwin/isabelle/init.bat
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/isabelle/init.bat	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,11 @@
+@echo off
+
+cd "%~dp0"
+cd "..\.."
+
+set CYGWIN=nodosfilewarning
+
+echo Initializing Cygwin ...
+"cygwin\bin\dash" /isabelle/rebaseall contrib/polyml-5.5.0
+"cygwin\bin\bash" /isabelle/postinstall
+
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/Cygwin/isabelle/postinstall
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/isabelle/postinstall	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,8 @@
+#!/bin/dash
+
+PATH=/bin
+
+bash /etc/postinstall/base-files-mketc.sh.done
+
+mkpasswd -l >/etc/passwd
+mkgroup -l >/etc/group
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/Cygwin/isabelle/rebaseall
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/isabelle/rebaseall	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,14 @@
+#!/bin/dash
+
+PATH=/bin
+
+FILE_LIST="$(mktemp)"
+
+for DIR in "$@"
+do
+  find "$DIR" -name "*.dll" >> "$FILE_LIST"
+done
+
+dash /bin/rebaseall -T "$FILE_LIST"
+
+rm -f "$FILE_LIST"
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/Cygwin/sfx.txt
--- a/Admin/Windows/Cygwin/sfx.txt	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/Cygwin/sfx.txt	Fri Jan 11 13:24:16 2013 +0100
@@ -1,9 +1,9 @@
 ;!@Install@!UTF-8!
 GUIFlags="64"
 InstallPath="%UserDesktop%"
-BeginPrompt="Unpack Isabelle2012?"
+BeginPrompt="Unpack Isabelle2013?"
 ExtractPathText="Target directory"
-ExtractTitle="Unpacking Isabelle2012 ..."
-Shortcut="Du,{%%T\Isabelle2012\Isabelle.exe},{},{},{},{},{%%T\Isabelle2012}"
-RunProgram="\"%%T\Isabelle2012\contrib\cygwin-1.7.9\init.bat\""
+ExtractTitle="Unpacking Isabelle2013 ..."
+Shortcut="Du,{%%T\Isabelle2013\Isabelle2013.exe},{},{},{},{},{%%T\Isabelle2013}"
+RunProgram="\"%%T\Isabelle2013\cygwin\init.bat\""
 ;!@InstallEnd@!
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/launch4j/Isabelle.exe
Binary file Admin/Windows/launch4j/Isabelle.exe has changed
diff -r 5601ae592679 -r e8d641235191 Admin/Windows/launch4j/isabelle.xml
--- a/Admin/Windows/launch4j/isabelle.xml	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/launch4j/isabelle.xml	Fri Jan 11 13:24:16 2013 +0100
@@ -20,11 +20,11 @@
     <cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
   </classPath>
   <jre>
-    <path>%EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
+    <path>%EXEDIR%\contrib\jdk-7u9\x86-cygwin\jdk1.7.0_09</path>
     <minVersion></minVersion>
     <maxVersion></maxVersion>
     <jdkPreference>jdkOnly</jdkPreference>
-    <opt>-Disabelle.home=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\\contrib\\cygwin-1.7.9&quot;</opt>
+    <opt>-Disabelle.home=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\\cygwin&quot;</opt>
   </jre>
   <splash>
     <file>isabelle.bmp</file>
diff -r 5601ae592679 -r e8d641235191 Admin/components/bundled
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/bundled	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,3 @@
+#additional components to be bundled for release
+ProofGeneral-4.1
+
diff -r 5601ae592679 -r e8d641235191 Admin/components/bundled-windows
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/bundled-windows	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,3 @@
+#additional components to be bundled for release
+cygwin-20130110
+
diff -r 5601ae592679 -r e8d641235191 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/components/components.sha1	Fri Jan 11 13:24:16 2013 +0100
@@ -1,4 +1,5 @@
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
+842d9526f37b928cf9e22f141884365129990d63  cygwin-20130110.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
 b98a98025d1f7e560ca6864a53296137dae736b4  e-1.6.tar.gz
 6d34b18ca0aa1e10bab6413045d079188c0e2dfb  exec_process-1.0.1.tar.gz
diff -r 5601ae592679 -r e8d641235191 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/lib/Tools/makedist	Fri Jan 11 13:24:16 2013 +0100
@@ -32,7 +32,7 @@
   echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
   echo "  the default is RELEASE if given, otherwise \"tip\"."
   echo
-  echo "  Auxiliary components are that of the running Isabelle version!"
+  echo "  Add-on components are that of the running Isabelle version!"
   echo
   exit 1
 }
@@ -170,17 +170,14 @@
 ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
   ./Admin/build all || fail "Failed to build distribution"
 
-if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
-  ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
-    ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
-else
-  echo "### Missing jEdit build component"
-fi
+./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
+  ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
 
-cp -a src/Doc src/Doc.orig
-./bin/isabelle env ./bin/isabelle build_doc -a || fail "Failed to build documentation"
-rm -rf src/Doc
-mv src/Doc.orig src/Doc
+cp -a src src.orig
+env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
+  ./bin/isabelle build_doc $JOBS -a || fail "Failed to build documentation"
+rm -rf src
+mv src.orig src
 
 rm -rf Admin
 
diff -r 5601ae592679 -r e8d641235191 Admin/lib/Tools/makedist_bundles
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/makedist_bundles	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,174 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: re-package Isabelle distribution with add-on components
+
+## diagnostics
+
+PRG=$(basename "$0")
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG ARCHIVE"
+  echo
+  echo "  Re-package Isabelle source distribution with add-on components"
+  echo "  and post-hoc patches for platform families linux, macos, windows."
+  echo
+  echo "  Add-on components are that of the running Isabelle version!"
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## arguments
+
+[ "$#" -ne 1 ] && usage
+
+ARCHIVE="$1"; shift
+
+[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
+
+ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
+ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
+
+
+## main
+
+for PLATFORM_FAMILY in linux macos windows
+do
+
+echo
+echo "*** $PLATFORM_FAMILY ***"
+
+TMP="/var/tmp/isabelle-makedist$$"
+mkdir "$TMP" || fail "Cannot create directory $TMP"
+
+ISABELLE_TARGET="$TMP/$ISABELLE_NAME"
+
+tar -C "$TMP" -x -z -f "$ARCHIVE"
+
+
+# bundled components
+
+mkdir -p "$ARCHIVE_DIR/contrib"
+
+echo "#bundled components" >> "$ISABELLE_TARGET/etc/components"
+
+for CATALOG in main "$PLATFORM_FAMILY" bundled "bundled-$PLATFORM_FAMILY"
+do
+  CATALOG_FILE="$ISABELLE_HOME/Admin/components/$CATALOG"
+  if [ -f "$CATALOG_FILE" ]
+  then
+    echo "catalog ${CATALOG}"
+    {
+      while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+      do
+        case "$REPLY" in
+          \#* | "") ;;
+          *)
+            COMPONENT="$REPLY"
+            case "$COMPONENT" in
+              jedit_build*) ;;
+              *)
+                echo "  component $COMPONENT"
+                CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"
+                if [ ! -f "$CONTRIB" ]; then
+                  REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz"
+                  echo "  download $REMOTE"
+                  perl -MLWP::Simple -e "getprint '$REMOTE';" > "$CONTRIB"
+                  perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2
+                fi
+
+                tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB"
+                echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
+                ;;
+            esac
+            ;;
+        esac
+      done
+    } < "$CATALOG_FILE"
+  fi
+done
+
+
+# platform-specific patches
+
+case "$PLATFORM_FAMILY" in
+  linux)
+    OTHER_PLATFORMS='-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
+    ;;
+  macos)
+    OTHER_PLATFORMS='-name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
+
+    perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
+      -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
+      -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
+      "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
+    ;;
+  windows)
+    OTHER_PLATFORMS='-name "x86*-linux" -o -name "x86*-darwin"'
+
+    perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
+      "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
+
+    mv "$ISABELLE_TARGET/contrib/cygwin" "$ISABELLE_TARGET"
+
+    cp "$ISABELLE_HOME/Admin/Windows/launch4j/Isabelle.exe" "$ISABELLE_TARGET/Isabelle2013.exe"
+    cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
+      "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
+
+    for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README
+    do
+      FILE="$ISABELLE_TARGET/$NAME"
+      {
+        echo '<?xml version="1.0" encoding="utf-8" ?>'
+        echo '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'
+        echo '<html xmlns="http://www.w3.org/1999/xhtml">'
+        echo '<head>'
+        echo '<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>'
+        echo "<title>${NAME}</title>"
+        echo '</head>'
+        echo '<body>'
+        echo '<pre>'
+        perl -w -p -e "s/&/&amp;/g; s/</&lt;/g; s/>/&gt;/g; s/'/&apos;/g; s/\"/&quot;/g;" "$FILE"
+        echo '</pre>'
+        echo '</body>'
+      } > "${FILE}.html"
+    done
+    ;;
+  *)
+    ;;
+esac
+
+
+# purge other platforms
+
+(
+  cd "$ISABELLE_TARGET"
+  for DIR in $(eval find contrib $OTHER_PLATFORMS | sort)
+  do
+    echo "removing $DIR"
+    rm -rf "$DIR"
+  done
+)
+
+
+# archive
+
+BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz"
+
+echo "packaging $(basename "$BUNDLE_ARCHIVE")"
+tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME"
+
+
+# clean up
+rm -rf "$TMP"
+
+done
+
diff -r 5601ae592679 -r e8d641235191 Admin/lib/Tools/makedist_cygwin
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/makedist_cygwin	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: produce pre-canned Cygwin distribution for Isabelle
+
+## diagnostics
+
+PRG=$(basename "$0")
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG"
+  echo
+  echo "  Produce pre-canned Cygwin distribution for Isabelle."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## arguments
+
+[ "$#" -ne 0 ] && usage
+
+
+## main
+
+TARGET="$PWD/cygwin"
+
+
+# download
+
+[ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\""
+mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\""
+
+perl -MLWP::Simple -e "getprint 'http://cygwin.com/setup.exe';" > "$TARGET/isabelle/cygwin.exe"
+chmod +x "$TARGET/isabelle/cygwin.exe"
+
+"$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
+
+
+# install
+
+"$TARGET/isabelle/cygwin.exe" \
+  --local-package-dir "$(cygpath -w "$TMP/cygwin")" \
+  --root "$(cygpath -w "$TARGET")" \
+  --packages libgmp3,perl,python,rlwrap \
+  --no-shortcuts --no-startmenu --no-desktop --quiet-mode
+
+[ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
+
+
+# patches
+
+for NAME in hosts protocols services networks
+do
+  rm "$TARGET/etc/$NAME"
+done
+
+ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll"
+
+rm "$TARGET/Cygwin.bat"
+
+cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/." "$TARGET/isabelle/."
+
+
+# archive
+
+tar cvzf "${TARGET}.tar.gz" "$TARGET"
diff -r 5601ae592679 -r e8d641235191 Isabelle
--- a/Isabelle	Thu Jan 10 21:22:11 2013 +0100
+++ b/Isabelle	Fri Jan 11 13:24:16 2013 +0100
@@ -4,5 +4,5 @@
 #
 # Default Isabelle application wrapper.
 
-exec "$(dirname "$0")"/bin/isabelle jedit "$@"
+exec "$(dirname "$0")"/bin/isabelle jedit -s "$@"
 
diff -r 5601ae592679 -r e8d641235191 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 11 13:24:16 2013 +0100
@@ -125,8 +125,8 @@
   { fix x :: "'n::euclidean_space"
     def y == "(e/norm x) *\<^sub>R x"
     then have "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto
-    moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
-    moreover hence "x = (norm x/e) *\<^sub>R y" by auto
+    moreover have *: "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
+    moreover from * have "x = (norm x/e) *\<^sub>R y" by auto
     ultimately have "x : span (cball 0 e)"
       using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
   } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto
@@ -297,7 +297,7 @@
     and "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
     and "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"
     and "setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
-  apply(rule_tac [!] setsum_cong2)
+  apply (rule_tac [!] setsum_cong2)
   using assms apply auto
   done
 
@@ -659,12 +659,12 @@
 qed
 
 lemma mem_affine:
-  assumes "affine S" "x : S" "y : S" "u+v=1"
+  assumes "affine S" "x : S" "y : S" "u + v = 1"
   shows "(u *\<^sub>R x + v *\<^sub>R y) : S"
   using assms affine_def[of S] by auto
 
 lemma mem_affine_3:
-  assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1"
+  assumes "affine S" "x : S" "y : S" "z : S" "u + v + w = 1"
   shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S"
 proof -
   have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}"
@@ -689,7 +689,9 @@
   "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
   unfolding subset_eq Ball_def
   unfolding affine_hull_explicit span_explicit mem_Collect_eq
-  apply (rule, rule) apply (erule exE)+ apply (erule conjE)+
+  apply (rule, rule)
+  apply (erule exE)+
+  apply (erule conjE)+
 proof -
   fix x t u
   assume as: "finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
@@ -1163,90 +1165,109 @@
   shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
 proof -
   let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
-  have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)
+  have Se: " \<exists>x. x \<in> ?S"
+    apply (rule exI[where x=a])
+    apply (auto simp add: fa)
+    done
   have Sub: "\<exists>y. isUb UNIV ?S y"
     apply (rule exI[where x= b])
-    using ab fb e12 by (auto simp add: isUb_def setle_def)
+    using ab fb e12 apply (auto simp add: isUb_def setle_def)
+    done
   from reals_complete[OF Se Sub] obtain l where
     l: "isLub UNIV ?S l"by blast
   have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12
     apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-    by (metis linorder_linear)
+    apply (metis linorder_linear)
+    done
   have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l
     apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-    by (metis linorder_linear not_le)
-    have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
-    have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
-    have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
-    then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
-    {assume le2: "f l \<in> e2"
-      from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
-      hence lap: "l - a > 0" using alb by arith
-      from e2[rule_format, OF le2] obtain e where
-        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
-      from dst[OF alb e(1)] obtain d where
-        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      let ?d' = "min (d/2) ((l - a)/2)"
-      have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
-        by (simp add: min_max.less_infI2)
-      then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
-      then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
-      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
-      from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
-      moreover
-      have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
-      ultimately have False using e12 alb d' by auto}
+    apply (metis linorder_linear not_le)
+    done
+  have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
+  have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
+  have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
+  then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
+  { assume le2: "f l \<in> e2"
+    from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
+    then have lap: "l - a > 0" using alb by arith
+    from e2[rule_format, OF le2] obtain e where
+      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
+    from dst[OF alb e(1)] obtain d where
+      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+    let ?d' = "min (d/2) ((l - a)/2)"
+    have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
+      by (simp add: min_max.less_infI2)
+    then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
+    then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
+    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
+    from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
     moreover
-    {assume le1: "f l \<in> e1"
+    have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
+    ultimately have False using e12 alb d' by auto }
+  moreover
+  { assume le1: "f l \<in> e1"
     from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
-      hence blp: "b - l > 0" using alb by arith
-      from e1[rule_format, OF le1] obtain e where
-        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
-      from dst[OF alb e(1)] obtain d where
-        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
-      then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
-      then obtain d' where d': "d' > 0" "d' < d" by metis
-      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
-      hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
-      with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
-      with l d' have False
-        by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
-    ultimately show ?thesis using alb by metis
+    then have blp: "b - l > 0" using alb by arith
+    from e1[rule_format, OF le1] obtain e where
+      e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
+    from dst[OF alb e(1)] obtain d where
+      d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+    have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
+    then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
+    then obtain d' where d': "d' > 0" "d' < d" by metis
+    from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
+    then have "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
+    with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
+    with l d' have False
+      by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
+  ultimately show ?thesis using alb by metis
 qed
 
 lemma convex_connected:
   fixes s :: "'a::real_normed_vector set"
   assumes "convex s" shows "connected s"
-proof-
-  { fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
+proof -
+  { fix e1 e2
+    assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
     assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
     then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>s" by auto
-    hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
+    then have n: "norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto
 
     { fix x e::real assume as:"0 \<le> x" "x \<le> 1" "0 < e"
-      { fix y have *:"(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2"
+      { fix y
+        have *: "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2"
           by (simp add: algebra_simps)
         assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
         hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
           unfolding * and scaleR_right_diff_distrib[symmetric]
-          unfolding less_divide_eq using n by auto  }
-      hence "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
-        apply(rule_tac x="e / norm (x1 - x2)" in exI) using as
-        apply auto unfolding zero_less_divide_iff using n by simp  }  note * = this
+          unfolding less_divide_eq using n by auto
+      }
+      then have "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
+        apply (rule_tac x="e / norm (x1 - x2)" in exI)
+        using as
+        apply auto
+        unfolding zero_less_divide_iff
+        using n apply simp
+        done
+    } note * = this
 
     have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
-      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
-      using * apply(simp add: dist_norm)
+      apply (rule connected_real_lemma)
+      apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
+      using * apply (simp add: dist_norm)
       using as(1,2)[unfolded open_dist] apply simp
       using as(1,2)[unfolded open_dist] apply simp
       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
-      using as(3) by auto
-    then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1"  "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" by auto
-    hence False using as(4)
+      using as(3) apply auto
+      done
+    then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1"  "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
+      by auto
+    then have False
+      using as(4)
       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]]
-      using x1(2) x2(2) by auto  }
-  thus ?thesis unfolding connected_def by auto
+      using x1(2) x2(2) by auto
+    }
+  then show ?thesis unfolding connected_def by auto
 qed
 
 text {* One rather trivial consequence. *}
@@ -1276,37 +1297,53 @@
   hence xy:"0 < dist x y" by (auto simp add: dist_nz[symmetric])
 
   then obtain u where "0 < u" "u \<le> 1" and u:"u < e / dist x y"
-    using real_lbound_gt_zero[of 1 "e / dist x y"] using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto
+    using real_lbound_gt_zero[of 1 "e / dist x y"]
+    using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto
   hence "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y" using `x\<in>s` `y\<in>s`
-    using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto
+    using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]]
+    by auto
   moreover
-  have *:"x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" by (simp add: algebra_simps)
-  have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`] unfolding dist_norm[symmetric]
+  have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
+    by (simp add: algebra_simps)
+  have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e"
+    unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`]
+    unfolding dist_norm[symmetric]
     using u unfolding pos_less_divide_eq[OF xy] by auto
-  hence "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto
-  ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
+  then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto
+  ultimately show False
+    using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
 qed
 
 lemma convex_ball:
   fixes x :: "'a::real_normed_vector"
   shows "convex (ball x e)"
-proof(auto simp add: convex_def)
-  fix y z assume yz:"dist x y < e" "dist x z < e"
-  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
-  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
-    using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
-  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto
+proof (auto simp add: convex_def)
+  fix y z
+  assume yz: "dist x y < e" "dist x z < e"
+  fix u v :: real
+  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
+    using uv yz
+    using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]]
+    by auto
+  then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
+    using convex_bound_lt[OF yz uv] by auto
 qed
 
 lemma convex_cball:
   fixes x :: "'a::real_normed_vector"
   shows "convex(cball x e)"
-proof(auto simp add: convex_def Ball_def)
-  fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"
-  fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
-  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
-    using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto
-  thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using convex_bound_le[OF yz uv] by auto
+proof (auto simp add: convex_def Ball_def)
+  fix y z
+  assume yz: "dist x y \<le> e" "dist x z \<le> e"
+  fix u v :: real
+  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+  have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
+    using uv yz
+    using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]]
+    by auto
+  then show "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
+    using convex_bound_le[OF yz uv] by auto
 qed
 
 lemma connected_ball:
@@ -1319,6 +1356,7 @@
   shows "connected(cball x e)"
   using convex_connected convex_cball by auto
 
+
 subsection {* Convex hull *}
 
 lemma convex_convex_hull: "convex(convex hull s)"
@@ -1326,102 +1364,182 @@
   by auto
 
 lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
-by (metis convex_convex_hull hull_same)
+  by (metis convex_convex_hull hull_same)
 
 lemma bounded_convex_hull:
   fixes s :: "'a::real_normed_vector set"
   assumes "bounded s" shows "bounded(convex hull s)"
-proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
-  show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
+proof -
+  from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
+    unfolding bounded_iff by auto
+  show ?thesis
+    apply (rule bounded_subset[OF bounded_cball, of _ 0 B])
     unfolding subset_hull[of convex, OF convex_cball]
-    unfolding subset_eq mem_cball dist_norm using B by auto qed
+    unfolding subset_eq mem_cball dist_norm using B apply auto
+    done
+qed
 
 lemma finite_imp_bounded_convex_hull:
   fixes s :: "'a::real_normed_vector set"
   shows "finite s \<Longrightarrow> bounded(convex hull s)"
   using bounded_convex_hull finite_imp_bounded by auto
 
+
 subsubsection {* Convex hull is "preserved" by a linear function *}
 
 lemma convex_hull_linear_image:
   assumes "bounded_linear f"
   shows "f ` (convex hull s) = convex hull (f ` s)"
-  apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
-  apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
-  apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
-proof-
+  apply rule
+  unfolding subset_eq ball_simps
+  apply (rule_tac[!] hull_induct, rule hull_inc)
+  prefer 3
+  apply (erule imageE)
+  apply (rule_tac x=xa in image_eqI)
+  apply assumption
+  apply (rule hull_subset[unfolded subset_eq, rule_format])
+  apply assumption
+proof -
   interpret f: bounded_linear f by fact
   show "convex {x. f x \<in> convex hull f ` s}"
-  unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
+    unfolding convex_def
+    by (auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format])
+next
   interpret f: bounded_linear f by fact
-  show "convex {x. x \<in> f ` (convex hull s)}" using  convex_convex_hull[unfolded convex_def, of s]
+  show "convex {x. x \<in> f ` (convex hull s)}"
+    using  convex_convex_hull[unfolded convex_def, of s]
     unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
 qed auto
 
 lemma in_convex_hull_linear_image:
   assumes "bounded_linear f" "x \<in> convex hull s"
   shows "(f x) \<in> convex hull (f ` s)"
-using convex_hull_linear_image[OF assms(1)] assms(2) by auto
+  using convex_hull_linear_image[OF assms(1)] assms(2) by auto
+
 
 subsubsection {* Stepping theorems for convex hulls of finite sets *}
 
 lemma convex_hull_empty[simp]: "convex hull {} = {}"
-  apply(rule hull_unique) by auto
+  by (rule hull_unique) auto
 
 lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
-  apply(rule hull_unique) by auto
+  by (rule hull_unique) auto
 
 lemma convex_hull_insert:
   fixes s :: "'a::real_vector set"
   assumes "s \<noteq> {}"
-  shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
-                                    b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
- apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof-
- fix x assume x:"x = a \<or> x \<in> s"
- thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer
-   apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
+  shows "convex hull (insert a s) =
+    {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
+  (is "?xyz = ?hull")
+  apply (rule, rule hull_minimal, rule)
+  unfolding insert_iff
+  prefer 3
+  apply rule
+proof -
+  fix x
+  assume x: "x = a \<or> x \<in> s"
+  then show "x \<in> ?hull"
+    apply rule
+    unfolding mem_Collect_eq
+    apply (rule_tac x=1 in exI)
+    defer
+    apply (rule_tac x=0 in exI)
+    using assms hull_subset[of s convex]
+    apply auto
+    done
 next
-  fix x assume "x\<in>?hull"
-  then obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto
-  have "a\<in>convex hull insert a s" "b\<in>convex hull insert a s"
-    using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto
-  thus "x\<in> convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def]
-    apply(erule_tac x=a in ballE) apply(erule_tac x=b in ballE) apply(erule_tac x=u in allE) using obt by auto
+  fix x
+  assume "x \<in> ?hull"
+  then obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b"
+    by auto
+  have "a \<in> convex hull insert a s" "b\<in>convex hull insert a s"
+    using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4)
+    by auto
+  then show "x \<in> convex hull insert a s"
+    unfolding obt(5)
+    using convex_convex_hull[of "insert a s", unfolded convex_def]
+    apply (erule_tac x = a in ballE)
+    apply (erule_tac x = b in ballE)
+    apply (erule_tac x = u in allE)
+    using obt apply auto
+    done
 next
-  show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
-    fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
-    from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
-    from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
-    have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
-    have "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
-    proof(cases "u * v1 + v * v2 = 0")
-      have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
-      case True hence **:"u * v1 = 0" "v * v2 = 0"
+  show "convex ?hull"
+    unfolding convex_def
+    apply (rule, rule, rule, rule, rule, rule, rule)
+  proof -
+    fix x y u v
+    assume as: "(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
+    from as(4) obtain u1 v1 b1
+      where obt1: "u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
+    from as(5) obtain u2 v2 b2
+      where obt2: "u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
+    have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
+      by (auto simp add: algebra_simps)
+    have **: "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y =
+      (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
+    proof (cases "u * v1 + v * v2 = 0")
+      case True
+      have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
+        by (auto simp add: algebra_simps)
+      from True have ***: "u * v1 = 0" "v * v2 = 0"
         using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by arith+
-      hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto
-      thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib)
+      then have "u * u1 + v * u2 = 1"
+        using as(3) obt1(3) obt2(3) by auto
+      then show ?thesis
+        unfolding obt1(5) obt2(5) *
+        using assms hull_subset[of s convex]
+        by (auto simp add: *** scaleR_right_distrib)
     next
-      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
-      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
-      also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
-      case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2" apply -
-        apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg)
-        using as(1,2) obt1(1,2) obt2(1,2) by auto
-      thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False
-        apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer
-        apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4)
+      case False
+      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)"
+        using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
+      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)"
+        using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
+      also have "\<dots> = u * v1 + v * v2"
+        by simp
+      finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
+      have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
+        apply (rule add_nonneg_nonneg)
+        prefer 4
+        apply (rule add_nonneg_nonneg)
+        apply (rule_tac [!] mult_nonneg_nonneg)
+        using as(1,2) obt1(1,2) obt2(1,2) apply auto
+        done
+      then show ?thesis
+        unfolding obt1(5) obt2(5)
+        unfolding * and **
+        using False
+        apply (rule_tac x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI)
+        defer
+        apply (rule convex_convex_hull[of s, unfolded convex_def, rule_format])
+        using obt1(4) obt2(4)
         unfolding add_divide_distrib[symmetric] and zero_le_divide_iff
-        by (auto simp add: scaleR_left_distrib scaleR_right_distrib)
-    qed note * = this
-    have u1:"u1 \<le> 1" unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
-    have u2:"u2 \<le> 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
-    have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono)
-      apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto
-    also have "\<dots> \<le> 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
-    finally
-    show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI)
-      apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def
-      using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
+        apply (auto simp add: scaleR_left_distrib scaleR_right_distrib)
+        done
+    qed
+    have u1: "u1 \<le> 1"
+      unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
+    have u2: "u2 \<le> 1"
+      unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
+    have "u1 * u + u2 * v \<le> (max u1 u2) * u + (max u1 u2) * v"
+      apply (rule add_mono)
+      apply (rule_tac [!] mult_right_mono)
+      using as(1,2) obt1(1,2) obt2(1,2)
+      apply auto
+      done
+    also have "\<dots> \<le> 1"
+      unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
+    finally show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
+      unfolding mem_Collect_eq
+      apply (rule_tac x="u * u1 + v * u2" in exI)
+      apply (rule conjI)
+      defer
+      apply (rule_tac x="1 - u * u1 - v * u2" in exI)
+      unfolding Bex_def
+      using as(1,2) obt1(1,2) obt2(1,2) **
+      apply (auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
+      done
   qed
 qed
 
@@ -1430,162 +1548,307 @@
 
 lemma convex_hull_indexed:
   fixes s :: "'a::real_vector set"
-  shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
-                            (setsum u {1..k} = 1) \<and>
-                            (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
-  apply(rule hull_unique) apply(rule) defer
-  apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
-proof-
-  fix x assume "x\<in>s"
-  thus "x \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
+  shows "convex hull s =
+    {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
+        (setsum u {1..k} = 1) \<and>
+        (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
+  apply (rule hull_unique)
+  apply rule
+  defer
+  apply (subst convex_def)
+  apply (rule, rule, rule, rule, rule, rule, rule)
+proof -
+  fix x
+  assume "x\<in>s"
+  then show "x \<in> ?hull"
+    unfolding mem_Collect_eq
+    apply (rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI)
+    apply auto
+    done
 next
-  fix t assume as:"s \<subseteq> t" "convex t"
-  show "?hull \<subseteq> t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof-
-    fix x k u y assume assm:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
-    show "x\<in>t" unfolding assm(3)[symmetric] apply(rule as(2)[unfolded convex, rule_format])
-      using assm(1,2) as(1) by auto qed
+  fix t
+  assume as: "s \<subseteq> t" "convex t"
+  show "?hull \<subseteq> t"
+    apply rule
+    unfolding mem_Collect_eq
+    apply (erule exE | erule conjE)+
+  proof -
+    fix x k u y
+    assume assm:
+      "\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s"
+      "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
+    show "x\<in>t"
+      unfolding assm(3) [symmetric]
+      apply (rule as(2)[unfolded convex, rule_format])
+      using assm(1,2) as(1) apply auto
+      done
+  qed
 next
-  fix x y u v assume uv:"0\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull"
-  from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto
-  from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto
-  have *:"\<And>P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
+  fix x y u v
+  assume uv: "0\<le>u" "0\<le>v" "u + v = (1::real)" and xy: "x\<in>?hull" "y\<in>?hull"
+  from xy obtain k1 u1 x1 where
+      x: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
+    by auto
+  from xy obtain k2 u2 x2 where
+      y: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
+    by auto
+  have *: "\<And>P (x1::'a) x2 s1 s2 i.
+    (if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
     "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
-    prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)
-  have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto
-  show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)
-    apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
-    apply(rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule)
-    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq
-    unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] proof-
-    fix i assume i:"i \<in> {1..k1+k2}"
-    show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
-    proof(cases "i\<in>{1..k1}")
-      case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto
-    next def j \<equiv> "i - k1"
-      case False with i have "j \<in> {1..k2}" unfolding j_def by auto
-      thus ?thesis unfolding j_def[symmetric] using False
-        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed
-  qed(auto simp add: not_le x(2,3) y(2,3) uv(3))
+    prefer 3
+    apply (rule, rule)
+    unfolding image_iff
+    apply (rule_tac x = "x - k1" in bexI)
+    apply (auto simp add: not_le)
+    done
+  have inj: "inj_on (\<lambda>i. i + k1) {1..k2}"
+    unfolding inj_on_def by auto
+  show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
+    apply rule
+    apply (rule_tac x="k1 + k2" in exI)
+    apply (rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
+    apply (rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI)
+    apply (rule, rule)
+    defer
+    apply rule
+    unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and
+      setsum_reindex[OF inj] and o_def Collect_mem_eq
+    unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric]
+  proof -
+    fix i
+    assume i: "i \<in> {1..k1+k2}"
+    show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and>
+      (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
+    proof (cases "i\<in>{1..k1}")
+      case True
+      then show ?thesis
+        using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto
+    next
+      case False
+      def j \<equiv> "i - k1"
+      from i False have "j \<in> {1..k2}" unfolding j_def by auto
+      then show ?thesis
+        unfolding j_def[symmetric]
+        using False
+        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]]
+        apply auto
+        done
+    qed
+  qed (auto simp add: not_le x(2,3) y(2,3) uv(3))
 qed
 
 lemma convex_hull_finite:
   fixes s :: "'a::real_vector set"
   assumes "finite s"
   shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
-         setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
-proof(rule hull_unique, auto simp add: convex_def[of ?set])
-  fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
-    apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
-    unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto
+    setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
+proof (rule hull_unique, auto simp add: convex_def[of ?set])
+  fix x
+  assume "x \<in> s"
+  then show "\<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
+    apply (rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI)
+    apply auto
+    unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms]
+    apply auto
+    done
 next
-  fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
-  fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
-  fix uy assume uy:"\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
-  { fix x assume "x\<in>s"
-    hence "0 \<le> u * ux x + v * uy x" using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
-      by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))  }
-  moreover have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
+  fix u v :: real
+  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+  fix ux assume ux: "\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
+  fix uy assume uy: "\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
+  { fix x
+    assume "x\<in>s"
+    then have "0 \<le> u * ux x + v * uy x"
+      using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
+      apply auto
+      apply (metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))
+      done
+  }
+  moreover
+  have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
     unfolding setsum_addf and setsum_right_distrib[symmetric] and ux(2) uy(2) using uv(3) by auto
-  moreover have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
-    unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] by auto
-  ultimately show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
-    apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto
+  moreover
+  have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
+    unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric]
+    by auto
+  ultimately
+  show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and>
+      (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
+    apply (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI)
+    apply auto
+    done
 next
-  fix t assume t:"s \<subseteq> t" "convex t"
-  fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
-  thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
+  fix t
+  assume t: "s \<subseteq> t" "convex t"
+  fix u
+  assume u: "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
+  then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t"
+    using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
     using assms and t(1) by auto
 qed
 
+
 subsubsection {* Another formulation from Lars Schewe *}
 
 lemma setsum_constant_scaleR:
   fixes y :: "'a::real_vector"
   shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
-apply (cases "finite A")
-apply (induct set: finite)
-apply (simp_all add: algebra_simps)
-done
+  apply (cases "finite A")
+  apply (induct set: finite)
+  apply (simp_all add: algebra_simps)
+  done
 
 lemma convex_hull_explicit:
   fixes p :: "'a::real_vector set"
   shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
-             (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
-proof-
+    (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
+proof -
   { fix x assume "x\<in>?lhs"
-    then obtain k u y where obt:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
+    then obtain k u y where
+        obt: "\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
       unfolding convex_hull_indexed by auto
 
-    have fin:"finite {1..k}" by auto
-    have fin':"\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
-    { fix j assume "j\<in>{1..k}"
-      hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"
-        using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp
-        apply(rule setsum_nonneg) using obt(1) by auto }
+    have fin: "finite {1..k}" by auto
+    have fin': "\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
+    { fix j
+      assume "j\<in>{1..k}"
+      then have "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> y i = y j}"
+        using obt(1)[THEN bspec[where x=j]] and obt(2)
+        apply simp
+        apply (rule setsum_nonneg)
+        using obt(1)
+        apply auto
+        done
+    }
     moreover
     have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"
       unfolding setsum_image_gen[OF fin, symmetric] using obt(2) by auto
     moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
       using setsum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
       unfolding scaleR_left.setsum using obt(3) by auto
-    ultimately have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
-      apply(rule_tac x="y ` {1..k}" in exI)
-      apply(rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI) by auto
-    hence "x\<in>?rhs" by auto  }
+    ultimately
+    have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+      apply (rule_tac x="y ` {1..k}" in exI)
+      apply (rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI)
+      apply auto
+      done
+    then have "x\<in>?rhs" by auto
+  }
   moreover
   { fix y assume "y\<in>?rhs"
-    then obtain s u where obt:"finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
-
-    obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
-
-    { fix i::nat assume "i\<in>{1..card s}"
-      hence "f i \<in> s"  apply(subst f(2)[symmetric]) by auto
-      hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto  }
+    then obtain s u where
+      obt: "finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y" by auto
+
+    obtain f where f: "inj_on f {1..card s}" "f ` {1..card s} = s"
+      using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
+
+    { fix i :: nat
+      assume "i\<in>{1..card s}"
+      then have "f i \<in> s"
+        apply (subst f(2)[symmetric])
+        apply auto
+        done
+      then have "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto
+    }
     moreover have *:"finite {1..card s}" by auto
-    { fix y assume "y\<in>s"
-      then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto
-      hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto
-      hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
-      hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
-            "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
-        by (auto simp add: setsum_constant_scaleR)   }
-
-    hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
+    { fix y
+      assume "y\<in>s"
+      then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"]
+        by auto
+      then have "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}"
+        apply auto
+        using f(1)[unfolded inj_on_def]
+        apply(erule_tac x=x in ballE)
+        apply auto
+        done
+      then have "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
+      then have "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
+          "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
+        by (auto simp add: setsum_constant_scaleR)
+    }
+    then have "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
       unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
       unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
-      using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto
-
-    ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
-      apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastforce
-    hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto  }
+      using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u]
+      unfolding obt(4,5) by auto
+    ultimately
+    have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and>
+        (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
+      apply (rule_tac x="card s" in exI)
+      apply (rule_tac x="u \<circ> f" in exI)
+      apply (rule_tac x=f in exI)
+      apply fastforce
+      done
+    then have "y \<in> ?lhs" unfolding convex_hull_indexed by auto
+  }
   ultimately show ?thesis unfolding set_eq_iff by blast
 qed
 
+
 subsubsection {* A stepping theorem for that expansion *}
 
 lemma convex_hull_finite_step:
-  fixes s :: "'a::real_vector set" assumes "finite s"
+  fixes s :: "'a::real_vector set"
+  assumes "finite s"
   shows "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)
      \<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs")
-proof(rule, case_tac[!] "a\<in>s")
-  assume "a\<in>s" hence *:"insert a s = s" by auto
-  assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto
+proof (rule, case_tac[!] "a\<in>s")
+  assume "a\<in>s"
+  then have *:" insert a s = s" by auto
+  assume ?lhs
+  then show ?rhs
+    unfolding *
+    apply (rule_tac x=0 in exI)
+    apply auto
+    done
 next
-  assume ?lhs then obtain u where u:"\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto
-  assume "a\<notin>s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp
-    apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s` by auto
+  assume ?lhs
+  then obtain u where u: "\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y"
+    by auto
+  assume "a \<notin> s"
+  then show ?rhs
+    apply (rule_tac x="u a" in exI)
+    using u(1)[THEN bspec[where x=a]]
+    apply simp
+    apply (rule_tac x=u in exI)
+    using u[unfolded setsum_clauses(2)[OF assms]] and `a\<notin>s`
+    apply auto
+    done
 next
-  assume "a\<in>s" hence *:"insert a s = s" by auto
-  have fin:"finite (insert a s)" using assms by auto
-  assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
-  show ?lhs apply(rule_tac x="\<lambda>x. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin]
-    unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s` by auto
+  assume "a \<in> s"
+  then have *: "insert a s = s" by auto
+  have fin: "finite (insert a s)" using assms by auto
+  assume ?rhs
+  then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+    by auto
+  show ?lhs
+    apply (rule_tac x = "\<lambda>x. (if a = x then v else 0) + u x" in exI)
+    unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin]
+    unfolding setsum_clauses(2)[OF assms]
+    using uv and uv(2)[THEN bspec[where x=a]] and `a\<in>s`
+    apply auto
+    done
 next
-  assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
-  moreover assume "a\<notin>s" moreover have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
-    apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\<notin>s` by auto
-  ultimately show ?lhs apply(rule_tac x="\<lambda>x. if a = x then v else u x" in exI)  unfolding setsum_clauses(2)[OF assms] by auto
-qed
+  assume ?rhs
+  then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+    by auto
+  moreover
+  assume "a \<notin> s"
+  moreover
+  have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
+    apply (rule_tac setsum_cong2)
+    defer
+    apply (rule_tac setsum_cong2)
+    using `a \<notin> s`
+    apply auto
+    done
+  ultimately show ?lhs
+    apply (rule_tac x="\<lambda>x. if a = x then v else u x" in exI)
+    unfolding setsum_clauses(2)[OF assms]
+    apply auto
+    done
+qed
+
 
 subsubsection {* Hence some special cases *}
 
diff -r 5601ae592679 -r e8d641235191 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Num.thy	Fri Jan 11 13:24:16 2013 +0100
@@ -245,6 +245,12 @@
   numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" |
   numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"
 
+lemma numeral_code [code]:
+  "numeral One = 1"
+  "numeral (Bit0 n) = (let m = numeral n in m + m)"
+  "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"
+  by (simp_all add: Let_def)
+  
 lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
   apply (induct x)
   apply simp
@@ -1103,3 +1109,4 @@
   Num Arith
 
 end
+
diff -r 5601ae592679 -r e8d641235191 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 11 13:24:16 2013 +0100
@@ -29,6 +29,7 @@
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
+val max_suggestions = 1024
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
 *}
@@ -71,8 +72,16 @@
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params thys 1024
-      (prefix ^ "mash_mepo_suggestions")
+  generate_mepo_suggestions @{context} params thys max_suggestions
+      (prefix ^ "mepo_suggestions")
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
+      (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
 else
   ()
 *}
diff -r 5601ae592679 -r e8d641235191 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -42,8 +42,7 @@
       default_params ctxt []
     val prover = hd provers
     val slack_max_facts = generous_max_facts (the max_facts)
-    val sugg_path = sugg_file_name |> Path.explode
-    val lines = sugg_path |> File.read_lines
+    val lines = Path.explode sugg_file_name |> File.read_lines
     val css = clasimpset_rule_table_of ctxt
     val facts = all_facts ctxt true false Symtab.empty [] [] css
     val name_tabs = build_name_tables nickname_of_thm facts
@@ -88,8 +87,11 @@
           val (mash_facts, mash_unks) =
             find_mash_suggestions slack_max_facts suggs facts [] []
             |>> weight_mash_facts
-          val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
-          val mesh_facts = mesh_facts slack_max_facts mess
+          val mess =
+            [(mepo_weight, (mepo_facts, [])),
+             (mash_weight, (mash_facts, mash_unks))]
+          val mesh_facts =
+            mesh_facts (Thm.eq_thm o pairself snd) slack_max_facts mess
           val isar_facts =
             find_suggested_facts (map (rpair 1.0) isar_deps) facts
           (* adapted from "mirabelle_sledgehammer.ML" *)
diff -r 5601ae592679 -r e8d641235191 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -24,6 +24,7 @@
     Proof.context -> params -> int * int option -> theory list -> string -> unit
   val generate_mepo_suggestions :
     Proof.context -> params -> theory list -> int -> string -> unit
+  val generate_mesh_suggestions : int -> string -> string -> string -> unit
 end;
 
 structure MaSh_Export : MASH_EXPORT =
@@ -164,16 +165,17 @@
   generate_isar_or_prover_commands ctxt prover (SOME params)
 
 fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) thys
-                              max_facts file_name =
+                              max_suggs file_name =
   let
     val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
     val facts = all_facts ctxt
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
     val name_tabs = build_name_tables nickname_of_thm facts
-    fun do_fact ((_, th), old_facts) =
+    fun do_fact (j, ((_, th), old_facts)) =
       let
         val name = nickname_of_thm th
+        val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
         val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val isar_deps = isar_dependencies_of name_tabs th
@@ -185,13 +187,38 @@
             val suggs =
               old_facts
               |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
-                     max_facts NONE hyp_ts concl_t
+                     max_suggs NONE hyp_ts concl_t
               |> map (nickname_of_thm o snd)
           in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end
       end
     fun accum x (yss as ys :: _) = (x :: ys) :: yss
     val old_factss = tl (fold accum new_facts [old_facts])
-    val lines = Par_List.map do_fact (new_facts ~~ rev old_factss)
+    val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss))
   in File.write_list path lines end
 
+fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name
+                              mesh_file_name =
+  let
+    val mesh_path = Path.explode mesh_file_name
+    val _ = File.write mesh_path ""
+    fun do_fact (mash_line, mepo_line) =
+      let
+        val (mash_name, mash_suggs) =
+          extract_suggestions mash_line
+          ||> (map fst #> weight_mash_facts)
+        val (mepo_name, mepo_suggs) =
+          extract_suggestions mepo_line
+          ||> (map fst #> weight_mash_facts)
+        val _ =
+          if mash_name = mepo_name then () else error "Input files out of sync."
+        val mess =
+          [(mepo_weight, (mepo_suggs, [])),
+           (mash_weight, (mash_suggs, []))]
+        val mesh_suggs = mesh_facts (op =) max_suggs mess
+        val mesh_line = mash_name ^ ": " ^ space_implode " " mesh_suggs ^ "\n"
+      in File.append mesh_path mesh_line end
+    val mash_lines = Path.explode mash_file_name |> File.read_lines
+    val mepo_lines = Path.explode mepo_file_name |> File.read_lines
+  in List.app do_fact (mash_lines ~~ mepo_lines) end
+
 end;
diff -r 5601ae592679 -r e8d641235191 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -449,9 +449,11 @@
       end
   end;
 
-fun size_matters_for _ Ts = not (forall
-  (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
-    (*FIXME eliminate dynamic name reference*)
+val size_types = [@{type_name Enum.finite_1}, @{type_name Enum.finite_2},
+  @{type_name Enum.finite_3}, @{type_name Enum.finite_4}, @{type_name Enum.finite_5}];
+
+fun size_matters_for _ Ts =
+  not (forall (fn Type (tyco, []) => member (op =) size_types tyco | _ => false) Ts);
 
 val test_goals =
   Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
diff -r 5601ae592679 -r e8d641235191 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -344,12 +344,12 @@
   let
     fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
     fun add_plain canon alias =
-      Symtab.update (Thm.get_name_hint canon,
+      Symtab.update (Thm.get_name_hint alias,
                      name_of (if_thm_before canon alias))
     fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
     fun add_inclass (name, target) =
       fold (fn s => Symtab.update (s, target)) (un_class_ify name)
-    val prop_tab = fold_rev cons_thm facts Termtab.empty
+    val prop_tab = fold cons_thm facts Termtab.empty
     val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   in (plain_name_tab, inclass_name_tab) end
diff -r 5601ae592679 -r e8d641235191 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -49,8 +49,8 @@
   val find_suggested_facts :
     (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
   val mesh_facts :
-    int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list
-    -> ('a * thm) list
+    ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
+    -> 'a list
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val goal_of_thm : theory -> thm -> thm
@@ -81,6 +81,8 @@
   val is_mash_enabled : unit -> bool
   val mash_can_suggest_facts : Proof.context -> bool
   val generous_max_facts : int -> int
+  val mepo_weight : real
+  val mash_weight : real
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
     -> term -> fact list -> fact list
@@ -444,13 +446,13 @@
       map (apsnd (curry Real.* (1.0 / avg))) xs
     end
 
-fun mesh_facts max_facts [(_, (sels, unks))] =
+fun mesh_facts _ max_facts [(_, (sels, unks))] =
     map fst (take max_facts sels) @ take (max_facts - length sels) unks
-  | mesh_facts max_facts mess =
+  | mesh_facts eq max_facts mess =
     let
       val mess =
         mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
-      val fact_eq = Thm.eq_thm o pairself snd
+      val fact_eq = eq
       fun score_in fact (global_weight, ((sel_len, sels), unks)) =
         let
           fun score_at j =
@@ -769,7 +771,7 @@
     val unknown =
       raw_unknown
       |> fold (subtract (Thm.eq_thm_prop o pairself snd)) [chained, proximity]
-  in (mesh_facts max_facts mess, unknown) end
+  in (mesh_facts (Thm.eq_thm o pairself snd) max_facts mess, unknown) end
 
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
@@ -1054,6 +1056,9 @@
    later for various reasons. *)
 fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts div 2)
 
+val mepo_weight = 0.5
+val mash_weight = 0.5
+
 (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    Sledgehammer and Try. *)
 val min_secs_for_learning = 15
@@ -1106,10 +1111,12 @@
             hyp_ts concl_t facts
         |>> weight_mash_facts
       val mess =
-        [] |> (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I)
-           |> (if fact_filter <> mepoN then cons (0.5, (mash ())) else I)
+        [] |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
+               else I)
+           |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
+               else I)
     in
-      mesh_facts max_facts mess
+      mesh_facts (Thm.eq_thm o pairself snd) max_facts mess
       |> not (null add_ths) ? prepend_facts add_ths
     end
 
diff -r 5601ae592679 -r e8d641235191 src/Pure/General/socket_io.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/socket_io.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,87 @@
+(*  Title:      Pure/General/socket_io.ML
+    Author:     Timothy Bourke, NICTA
+    Author:     Makarius
+
+Stream IO over TCP sockets.  Following example 10.2 in "The Standard
+ML Basis Library" by Emden R. Gansner and John H. Reppy.
+
+Note: BinIO requires Poly/ML 5.5.x to work reliably.
+*)
+
+signature SOCKET_IO =
+sig
+  val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream
+  val open_streams: string -> BinIO.instream * BinIO.outstream
+end;
+
+structure Socket_IO: SOCKET_IO =
+struct
+
+fun make_streams socket =
+  let
+    val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket);
+    val name = NetHostDB.toString host ^ ":" ^ string_of_int port;
+
+    val rd =
+      BinPrimIO.RD {
+        name = name,
+        chunkSize = Socket.Ctl.getRCVBUF socket,
+        readVec = SOME (fn n => Socket.recvVec (socket, n)),
+        readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
+        readVecNB = NONE,
+        readArrNB = NONE,
+        block = NONE,
+        canInput = NONE,
+        avail = fn () => NONE,
+        getPos = NONE,
+        setPos = NONE,
+        endPos = NONE,
+        verifyPos = NONE,
+        close = fn () => Socket.close socket,
+        ioDesc = NONE
+      };
+
+    val wr =
+      BinPrimIO.WR {
+        name = name,
+        chunkSize = Socket.Ctl.getSNDBUF socket,
+        writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
+        writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
+        writeVecNB = NONE,
+        writeArrNB = NONE,
+        block = NONE,
+        canOutput = NONE,
+        getPos = NONE,
+        setPos = NONE,
+        endPos = NONE,
+        verifyPos = NONE,
+        close = fn () => Socket.close socket,
+        ioDesc = NONE
+      };
+
+    val in_stream =
+      BinIO.mkInstream
+        (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList []));
+
+    val out_stream =
+      BinIO.mkOutstream
+        (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF));
+
+  in (in_stream, out_stream) end;
+
+
+fun open_streams socket_name =
+  let
+    fun err () = error ("Bad socket name: " ^ quote socket_name);
+    val (host, port) =
+      (case space_explode ":" socket_name of
+        [h, p] =>
+         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
+          case Int.fromString p of SOME port => port | NONE => err ())
+      | _ => err ());
+    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
+    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
+  in make_streams socket end;
+
+end;
+
diff -r 5601ae592679 -r e8d641235191 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -257,13 +257,6 @@
 
 (* Sockets *)
 
-structure Socket =
-struct
-  open Socket;
-  fun recvVec (a, b) = Socket.recvVec (a, dest_int b);
-  fun sendVec a = mk_int (Socket.sendVec a);
-end;
-
 structure INetSock =
 struct
   open INetSock;
diff -r 5601ae592679 -r e8d641235191 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/ROOT	Fri Jan 11 13:24:16 2013 +0100
@@ -87,6 +87,7 @@
     "General/seq.ML"
     "General/sha1.ML"
     "General/sha1_polyml.ML"
+    "General/socket_io.ML"
     "General/source.ML"
     "General/stack.ML"
     "General/symbol.ML"
diff -r 5601ae592679 -r e8d641235191 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/ROOT.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -57,6 +57,7 @@
 use "General/file.ML";
 use "General/long_name.ML";
 use "General/binding.ML";
+use "General/socket_io.ML";
 
 use "General/sha1.ML";
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
diff -r 5601ae592679 -r e8d641235191 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/System/options.scala	Fri Jan 11 13:24:16 2013 +0100
@@ -63,8 +63,9 @@
   private val SECTION = "section"
   private val OPTION = "option"
   private val OPTIONS = Path.explode("etc/options")
-  private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
-  private val PREFS_BACKUP = Path.explode("$ISABELLE_HOME_USER/etc/preferences~")
+  private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
+  private val PREFS = PREFS_DIR + Path.basic("preferences")
+  private val PREFS_BACKUP = PREFS_DIR + Path.basic("preferences~")
 
   lazy val options_syntax =
     Outer_Syntax.init() + ":" + "=" + "--" +
@@ -347,6 +348,7 @@
       changed.sortBy(_._1)
         .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
 
+    Options.PREFS_DIR.file.mkdirs()
     Options.PREFS.file renameTo Options.PREFS_BACKUP.file
     File.write(Options.PREFS,
       "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
diff -r 5601ae592679 -r e8d641235191 src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/System/system_channel.ML	Fri Jan 11 13:24:16 2013 +0100
@@ -47,65 +47,31 @@
   end;
 
 
-(* sockets *)  (* FIXME proper buffering via BinIO (after Poly/ML 5.4.1) *)
+(* sockets *)
 
-local
-
-fun readN socket n =
+fun read_line in_stream =
   let
-    fun read i buf =
-      let
-        val s = Byte.bytesToString (Socket.recvVec (socket, n - i));
-        val m = size s;
-        val i' = i + m;
-        val buf' = Buffer.add s buf;
-      in if m > 0 andalso n > i' then read i' buf' else Buffer.content buf' end;
-  in read 0 Buffer.empty end;
-
-fun read_line socket =
-  let
-    fun result cs = implode (rev ("\n" :: cs));
+    fun result cs = String.implode (rev (#"\n" :: cs));
     fun read cs =
-      (case readN socket 1 of
-        "" => if null cs then NONE else SOME (result cs)
-      | "\n" => SOME (result cs)
-      | c => read (c :: cs));
+      (case BinIO.input1 in_stream of
+        NONE => if null cs then NONE else SOME (result cs)
+      | SOME b =>
+          (case Byte.byteToChar b of
+            #"\n" => SOME (result cs)
+          | c => read (c :: cs)));
   in read [] end;
 
-fun write socket =
-  let
-    fun send buf =
-      if Word8VectorSlice.isEmpty buf then ()
-      else
-        let
-          val n = Int.min (Word8VectorSlice.length buf, 4096);
-          val m = Socket.sendVec (socket, Word8VectorSlice.subslice (buf, 0, SOME n));
-          val buf' = Word8VectorSlice.subslice (buf, m, NONE);
-        in send buf' end;
-  in fn s => send (Word8VectorSlice.full (Byte.stringToBytes s)) end;
-
-in
-
 fun socket_rendezvous name =
   let
-    fun err () = error ("Bad socket name: " ^ quote name);
-    val (host, port) =
-      (case space_explode ":" name of
-        [h, p] =>
-         (case NetHostDB.getByName h of SOME host => host | NONE => err (),
-          case Int.fromString p of SOME port => port | NONE => err ())
-      | _ => err ());
-    val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
-    val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
+    val (in_stream, out_stream) = Socket_IO.open_streams name;
+    val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
   in
     System_Channel
-     {input_line = fn () => read_line socket,
-      inputN = fn n => readN socket n,
-      output = fn s => write socket s,
-      flush = fn () => ()}
+     {input_line = fn () => read_line in_stream,
+      inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)),
+      output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
+      flush = fn () => BinIO.flushOut out_stream}
   end;
 
 end;
 
-end;
-
diff -r 5601ae592679 -r e8d641235191 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/Tools/main.scala	Fri Jan 11 13:24:16 2013 +0100
@@ -17,7 +17,7 @@
       try {
         Platform.init_laf()
         Isabelle_System.init()
-        Isabelle_System.isabelle_tool("jedit", args: _*)
+        Isabelle_System.isabelle_tool("jedit", ("-s" :: args.toList): _*)
       }
       catch { case exn: Throwable => (Exn.message(exn), 2) }
 
diff -r 5601ae592679 -r e8d641235191 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Jan 11 13:24:16 2013 +0100
@@ -306,12 +306,11 @@
 
 ## main
 
-# perspective
+if [ "$BUILD_ONLY" = false ]; then
+  mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"
 
-mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"
-
-if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
-  cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
+  if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
+    cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
 <DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
 EOF
   cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
@@ -323,12 +322,8 @@
 </VIEW>
 </PERSPECTIVE>
 EOF
-fi
-
+  fi
 
-# main
-
-if [ "$BUILD_ONLY" = false ]; then
   if [ "$NO_BUILD" = false ]; then
     "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"
     RC="$?"
diff -r 5601ae592679 -r e8d641235191 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Jan 11 13:24:16 2013 +0100
@@ -7,6 +7,7 @@
 buffer.noTabs=true
 buffer.sidekick.keystroke-parse=false
 buffer.tabSize=2
+console.dock-position=floating
 console.encoding=UTF-8
 console.font=IsabelleText
 console.fontsize=14
@@ -182,7 +183,7 @@
 isabelle-output.width=412
 isabelle-readme.dock-position=bottom
 isabelle-symbols.dock-position=bottom
-isabelle-theories.dock-position=bottom
+isabelle-theories.dock-position=right
 isabelle.cancel-execution.label=Cancel execution
 isabelle.cancel-execution.shortcut=C+e BACK_SPACE
 isabelle.check-buffer.label=Commence full checking
diff -r 5601ae592679 -r e8d641235191 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Jan 11 13:24:16 2013 +0100
@@ -189,9 +189,9 @@
       react {
         case phase: Session.Phase =>
           phase match {
-            case Session.Failed =>
+            case Session.Inactive | Session.Failed =>
               Swing_Thread.later {
-                Library.error_dialog(jEdit.getActiveView, "Prover process failure",
+                Library.error_dialog(jEdit.getActiveView, "Prover process terminated",
                     "Isabelle Syslog", Library.scrollable_text(PIDE.session.current_syslog()))
               }