# HG changeset patch
# User wenzelm
# Date 1379012066 -7200
# Node ID fcd36f587512f8759f28ea016ca5db54f97f6454
# Parent  773302e7741d1e09848674cbda8488bd1fb5cbb6# Parent  1f381570343654f2e29aaf25f515bab71c68982f
merged;

diff -r 773302e7741d -r fcd36f587512 Admin/Linux/Isabelle
--- a/Admin/Linux/Isabelle	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/Linux/Isabelle	Thu Sep 12 20:54:26 2013 +0200
@@ -4,25 +4,24 @@
 #
 # Main Isabelle application wrapper.
 
+# dereference executable
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 
-## settings
-
-PRG="$(basename "$0")"
+# minimal Isabelle environment
 
 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
 
 
-## main
+# main
 
-declare -a JAVA_ARGS
-JAVA_ARGS=({JAVA_ARGS})
+exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
+  "-Disabelle.home=$ISABELLE_HOME" \
+  {JAVA_ARGS} \
+  -classpath "{CLASSPATH}" \
+  isabelle.Main "$@"
 
-exec "$ISABELLE_HOME/bin/isabelle" java "${JAVA_ARGS[@]}" \
-  -classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" isabelle.Main "$@"
-
diff -r 773302e7741d -r fcd36f587512 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/Release/CHECKLIST	Thu Sep 12 20:54:26 2013 +0200
@@ -11,6 +11,8 @@
 
 - test 'display_drafts' command;
 
+- test "#!/usr/bin/env isabelle_scala_script";
+
 - check HTML header of library;
 
 - check file positions within logic images (hyperlinks etc.);
diff -r 773302e7741d -r fcd36f587512 Admin/Windows/WinRun4J/Isabelle.ini
--- a/Admin/Windows/WinRun4J/Isabelle.ini	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/Windows/WinRun4J/Isabelle.ini	Thu Sep 12 20:54:26 2013 +0200
@@ -1,11 +1,4 @@
 main.class=isabelle.Main
-classpath.1=lib\classes\ext\Pure.jar
-classpath.2=lib\classes\ext\scala-compiler.jar
-classpath.3=lib\classes\ext\scala-library.jar
-classpath.4=lib\classes\ext\scala-swing.jar
-classpath.5=lib\classes\ext\scala-actors.jar
-classpath.6=lib\classes\ext\scala-reflect.jar
-classpath.7=src\Tools\jEdit\dist\jedit.jar
 vm.location=contrib\jdk\x86-cygwin\jre\bin\server\jvm.dll
 splash.image=lib\logo\isabelle.bmp
 vmarg.1=-Disabelle.home=%INI_DIR%
diff -r 773302e7741d -r fcd36f587512 Admin/build
--- a/Admin/build	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/build	Thu Sep 12 20:54:26 2013 +0200
@@ -74,7 +74,7 @@
 
 ## main
 
-#workaround for scalac
+#workaround for scalac 2.10.2
 function stty() { :; }
 export -f stty
 
diff -r 773302e7741d -r fcd36f587512 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/components/components.sha1	Thu Sep 12 20:54:26 2013 +0200
@@ -34,6 +34,7 @@
 c85c0829b8170f25aa65ec6852f505ce2a50639b  jedit_build-20130628.tar.gz
 5de3e399be2507f684b49dfd13da45228214bbe4  jedit_build-20130905.tar.gz
 87136818fd5528d97288f5b06bd30c787229eb0d  jedit_build-20130910.tar.gz
+0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz
@@ -59,6 +60,7 @@
 e6a43b7b3b21295853bd2a63b27ea20bd6102f5f  windows_app-20130906.tar.gz
 8fe004aead867d4c82425afac481142bd3f01fb0  windows_app-20130908.tar.gz
 d273abdc7387462f77a127fa43095eed78332b5c  windows_app-20130909.tar.gz
+1c36a840320dfa9bac8af25fc289a4df5ea3eccb  xz-java-1.2-1.tar.gz
 2ae13aa17d0dc95ce254a52f1dba10929763a10d  xz-java-1.2.tar.gz
 4530a1aa6f4498ee3d78d6000fa71a3f63bd077f  yices-1.0.28.tar.gz
 12ae71acde43bd7bed1e005c43034b208c0cba4c  z3-3.2.tar.gz
diff -r 773302e7741d -r fcd36f587512 Admin/components/main
--- a/Admin/components/main	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/components/main	Thu Sep 12 20:54:26 2013 +0200
@@ -5,10 +5,10 @@
 Haskabelle-2013
 jdk-7u25
 jedit_build-20130910
-jfreechart-1.0.14
+jfreechart-1.0.14-1
 kodkodi-1.5.2
 polyml-5.5.0-3
 scala-2.10.2
 spass-3.8ds
 z3-3.2
-xz-java-1.2
+xz-java-1.2-1
diff -r 773302e7741d -r fcd36f587512 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/lib/Tools/makedist	Thu Sep 12 20:54:26 2013 +0200
@@ -168,6 +168,8 @@
 find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
 find . -print | xargs chmod -f u+rw
 
+export CLASSPATH="$ISABELLE_CLASSPATH"
+
 ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \
   ./Admin/build all || fail "Failed to build distribution"
 
diff -r 773302e7741d -r fcd36f587512 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Thu Sep 12 17:36:06 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Thu Sep 12 20:54:26 2013 +0200
@@ -51,6 +51,30 @@
 tar -C "$TMP" -x -z -f "$ARCHIVE" || exit 2
 
 
+# distribution classpath (based on educated guesses)
+
+splitarray ":" "$ISABELLE_CLASSPATH"; CLASSPATH_ENTRIES=("${SPLITARRAY[@]}")
+declare -a DISTRIBITION_CLASSPATH=()
+
+for ENTRY in "${CLASSPATH_ENTRIES[@]}"
+do
+  ENTRY=$(echo "$ENTRY" | perl -n -e "
+    if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; }
+    elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; }
+    else { print; };
+    print qq{\n};")
+  DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY"
+done
+
+DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="src/Tools/jEdit/dist/jedit.jar"
+
+echo "classpath"
+for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
+do
+  echo "  $ENTRY"
+done
+
+
 # bundled components
 
 init_component "$JEDIT_HOME"
@@ -128,9 +152,19 @@
 case "$PLATFORM_FAMILY" in
   linux)
     purge_contrib '-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
+
+    LINUX_CLASSPATH=""
+    for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
+    do
+      if [ -z "$LINUX_CLASSPATH" ]; then
+        LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY"
+      else
+        LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY"
+      fi
+    done
     cat "$ISABELLE_HOME/Admin/Linux/Isabelle" | \
-      perl -p -e "s,{JAVA_ARGS},$JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS,g;" \
-        > "$ISABELLE_TARGET/$ISABELLE_NAME"
+      perl -p > "$ISABELLE_TARGET/$ISABELLE_NAME" \
+        -e "s,{JAVA_ARGS},$JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS,g; s,{CLASSPATH},$LINUX_CLASSPATH,;"
     chmod +x "$ISABELLE_TARGET/$ISABELLE_NAME"
     ;;
   macos)
@@ -151,6 +185,7 @@
 
     (
       cat "$ISABELLE_HOME/Admin/Windows/WinRun4J/Isabelle.ini"
+
       declare -a JAVA_ARGS=()
       eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
       A=2
@@ -159,6 +194,14 @@
         echo -e "vmarg.$A=$ARG\r"
         A=$[ $A + 1 ]
       done
+
+      A=1
+      for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
+      do
+        ENTRY=$(echo "$ENTRY" | perl -p -e 's,/,\\\\,g;')
+        echo -e "classpath.$A=$ENTRY\r"
+        A=$[ $A + 1 ]
+      done
     ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.ini"
 
     cp "$TMP/windows_app/Isabelle.exe" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe"
@@ -233,11 +276,10 @@
           cat "$APP_TEMPLATE/Info.plist-part2"
         ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
 
-        for NAME in Pure.jar scala-compiler.jar scala-library.jar scala-swing.jar scala-actors.jar scala-reflect.jar
+        for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
         do
-          ln -sf "../Resources/${ISABELLE_NAME}/lib/classes/ext/$NAME" "$APP/Contents/Java"
+          ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$APP/Contents/Java"
         done
-        ln -sf "../Resources/${ISABELLE_NAME}/src/Tools/jEdit/dist/jedit.jar" "$APP/Contents/Java"
 
         cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
         cp "$APP_TEMPLATE/../isabelle.icns" "$APP/Contents/Resources/."
diff -r 773302e7741d -r fcd36f587512 etc/settings
--- a/etc/settings	Thu Sep 12 17:36:06 2013 +0200
+++ b/etc/settings	Thu Sep 12 20:54:26 2013 +0200
@@ -15,6 +15,13 @@
 
 ISABELLE_JAVA_SYSTEM_OPTIONS="-Dfile.encoding=UTF-8 -server"
 
+classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-library.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-swing.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-actors.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-compiler.jar"
+classpath "$ISABELLE_HOME/lib/classes/scala-reflect.jar"
+
 
 ###
 ### Interactive sessions (cf. isabelle tty)
diff -r 773302e7741d -r fcd36f587512 lib/Tools/java
--- a/lib/Tools/java	Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/Tools/java	Thu Sep 12 20:54:26 2013 +0200
@@ -4,9 +4,11 @@
 #
 # DESCRIPTION: invoke Java within the Isabelle environment
 
-CLASSPATH="$(jvmpath "$CLASSPATH")"
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
 
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
+[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
+unset CLASSPATH
+
 isabelle_jdk java "${JAVA_ARGS[@]}" \
-  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+  -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
 
diff -r 773302e7741d -r fcd36f587512 lib/Tools/scala
--- a/lib/Tools/scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/Tools/scala	Thu Sep 12 20:54:26 2013 +0200
@@ -6,6 +6,6 @@
 
 isabelle_admin_build jars || exit $?
 
-CLASSPATH="$(jvmpath "$CLASSPATH")"
 isabelle_scala scala -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+  -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
+
diff -r 773302e7741d -r fcd36f587512 lib/Tools/scalac
--- a/lib/Tools/scalac	Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/Tools/scalac	Thu Sep 12 20:54:26 2013 +0200
@@ -6,7 +6,6 @@
 
 isabelle_admin_build jars || exit $?
 
-CLASSPATH="$(jvmpath "$CLASSPATH")"
 isabelle_scala scalac -Dfile.encoding=UTF-8 \
-  "-Djava.ext.dirs=$(jvmpath "$ISABELLE_JAVA_EXT:$ISABELLE_HOME/lib/classes/ext")" "$@"
+  -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
 
diff -r 773302e7741d -r fcd36f587512 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Sep 12 17:36:06 2013 +0200
+++ b/lib/scripts/getsettings	Thu Sep 12 20:54:26 2013 +0200
@@ -21,16 +21,20 @@
   ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
   ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
 
-  CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
   function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
   CYGWIN_ROOT="$(jvmpath "/")"
+
+  ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
+  unset CLASSPATH
 else
   if [ -z "$USER_HOME" ]; then
     USER_HOME="$HOME"
   fi
 
   function jvmpath() { echo "$@"; }
-  CLASSPATH="$CLASSPATH"
+
+  ISABELLE_CLASSPATH="$CLASSPATH"
+  unset CLASSPATH
 fi
 
 export ISABELLE_HOME
@@ -122,18 +126,18 @@
   function isabelle_admin_build () { return 0; }
 fi
 
-#CLASSPATH convenience
+#classpath
 function classpath ()
 {
   for X in "$@"
   do
-    if [ -z "$CLASSPATH" ]; then
-      CLASSPATH="$X"
+    if [ -z "$ISABELLE_CLASSPATH" ]; then
+      ISABELLE_CLASSPATH="$X"
     else
-      CLASSPATH="$X:$CLASSPATH"
+      ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
     fi
   done
-  export CLASSPATH
+  export ISABELLE_CLASSPATH
 }
 
 #arrays
diff -r 773302e7741d -r fcd36f587512 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Doc/System/Scala.thy	Thu Sep 12 20:54:26 2013 +0200
@@ -61,10 +61,10 @@
 
   This allows to compile further Scala modules, depending on existing
   Isabelle/Scala functionality.  The resulting class or jar files can
-  be added to the @{setting CLASSPATH} via the @{verbatim classpath}
-  Bash function that is provided by the Isabelle process environment.
-  Thus add-on components can register themselves in a modular manner,
-  see also \secref{sec:components}.
+  be added to the Java classpath the @{verbatim classpath} Bash
+  function that is provided by the Isabelle process environment.  Thus
+  add-on components can register themselves in a modular manner, see
+  also \secref{sec:components}.
 
   Note that jEdit (\secref{sec:tool-jedit}) has its own mechanisms for
   adding plugin components, which needs special attention since
diff -r 773302e7741d -r fcd36f587512 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Thu Sep 12 20:54:26 2013 +0200
@@ -1,7 +1,8 @@
-(* Author:                     John Harrison
-   Translation from HOL light: Robert Himmelmann, TU Muenchen *)
+(*  Author:     John Harrison
+    Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
+*)
 
-header {* Fashoda meet theorem. *}
+header {* Fashoda meet theorem *}
 
 theory Fashoda
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
@@ -15,131 +16,312 @@
 lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
   by (auto simp add: Basis_vec_def axis_eq_axis)
 
-subsection {*Fashoda meet theorem. *}
+
+subsection {* Fashoda meet theorem *}
 
-lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
-  unfolding infnorm_cart UNIV_2 apply(rule cSup_eq) by auto
+lemma infnorm_2:
+  fixes x :: "real^2"
+  shows "infnorm x = max (abs (x$1)) (abs (x$2))"
+  unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
 
-lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
-        (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
+lemma infnorm_eq_1_2:
+  fixes x :: "real^2"
+  shows "infnorm x = 1 \<longleftrightarrow>
+    abs (x$1) \<le> 1 \<and> abs (x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
   unfolding infnorm_2 by auto
 
-lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
+lemma infnorm_eq_1_imp:
+  fixes x :: "real^2"
+  assumes "infnorm x = 1"
+  shows "abs (x$1) \<le> 1" and "abs (x$2) \<le> 1"
   using assms unfolding infnorm_eq_1_2 by auto
 
-lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
-  assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
-  "continuous_on {- 1..1} f"  "continuous_on {- 1..1} g"
-  "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
-  shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
-  case goal1 note as = this[unfolded bex_simps,rule_format]
+lemma fashoda_unit:
+  fixes f g :: "real \<Rightarrow> real^2"
+  assumes "f ` {- 1..1} \<subseteq> {- 1..1}"
+    and "g ` {- 1..1} \<subseteq> {- 1..1}"
+    and "continuous_on {- 1..1} f"
+    and "continuous_on {- 1..1} g"
+    and "f (- 1)$1 = - 1"
+    and "f 1$1 = 1" "g (- 1) $2 = -1"
+    and "g 1 $2 = 1"
+  shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t"
+proof (rule ccontr)
+  assume "\<not> ?thesis"
+  note as = this[unfolded bex_simps,rule_format]
   def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 
-  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" 
-  have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
+  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
+  have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
     unfolding negatex_def infnorm_2 vector_2 by auto
-  have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
-    unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] unfolding abs_inverse real_abs_infnorm
-    apply(subst infnorm_eq_0[THEN sym]) by auto
-  let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
-  have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
-    apply(rule set_eqI) unfolding image_iff Bex_def mem_interval_cart apply rule defer 
-    apply(rule_tac x="vec x" in exI) by auto
-  { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
+  have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
+    unfolding sqprojection_def
+    unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
+    unfolding abs_inverse real_abs_infnorm
+    apply (subst infnorm_eq_0[THEN sym])
+    apply auto
+    done
+  let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
+  have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
+    apply (rule set_eqI)
+    unfolding image_iff Bex_def mem_interval_cart
+    apply rule
+    defer
+    apply (rule_tac x="vec x" in exI)
+    apply auto
+    done
+  {
+    fix x
+    assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
     then guess w unfolding image_iff .. note w = this
-    hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this
-  have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
-  have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
-  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
-    apply(intro continuous_on_intros continuous_on_component)
-    unfolding * apply(rule assms)+
-    apply(subst sqprojection_def)
-    apply(intro continuous_on_intros)
-    apply(simp add: infnorm_eq_0 x0)
-    apply(rule linear_continuous_on)
-  proof-
-    show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
-      show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
-        apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) 
-        unfolding negatex_def by(auto simp add:vector_2 ) qed
+    then have "x \<noteq> 0"
+      using as[of "w$1" "w$2"]
+      unfolding mem_interval_cart
+      by auto
+  } note x0 = this
+  have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
+    using UNIV_2 by auto
+  have 1: "{- 1<..<1::real^2} \<noteq> {}"
+    unfolding interval_eq_empty_cart by auto
+  have 2: "continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
+    apply (intro continuous_on_intros continuous_on_component)
+    unfolding *
+    apply (rule assms)+
+    apply (subst sqprojection_def)
+    apply (intro continuous_on_intros)
+    apply (simp add: infnorm_eq_0 x0)
+    apply (rule linear_continuous_on)
+  proof -
+    show "bounded_linear negatex"
+      apply (rule bounded_linearI')
+      unfolding vec_eq_iff
+    proof (rule_tac[!] allI)
+      fix i :: 2
+      fix x y :: "real^2"
+      fix c :: real
+      show "negatex (x + y) $ i =
+        (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
+        apply -
+        apply (case_tac[!] "i\<noteq>1")
+        prefer 3
+        apply (drule_tac[1-2] 21) 
+        unfolding negatex_def
+        apply (auto simp add:vector_2)
+        done
+    qed
   qed
-  have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
-    case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
-    hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
-    have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
-    thus "x\<in>{- 1..1}" unfolding mem_interval_cart infnorm_2 apply- apply rule
-    proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
-  guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
-    apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval
-    apply(rule 1 2 3)+ . note x=this
-  have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
-  hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
-  have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
-  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"    "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
-    apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
-    have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
-    thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
+  have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}"
+    unfolding subset_eq
+    apply rule
+  proof -
+    case goal1
+    then guess y unfolding image_iff .. note y=this
+    have "?F y \<noteq> 0"
+      apply (rule x0)
+      using y(1)
+      apply auto
+      done
+    then have *: "infnorm (sqprojection (?F y)) = 1"
+      unfolding y o_def by - (rule lem2[rule_format])
+    have "infnorm x = 1"
+      unfolding *[THEN sym] y o_def by (rule lem1[rule_format])
+    then show "x \<in> {- 1..1}"
+      unfolding mem_interval_cart infnorm_2
+      apply -
+      apply rule
+    proof -
+      case goal1
+      then show ?case
+        apply (cases "i = 1")
+        defer
+        apply (drule 21)
+        apply auto
+        done
+    qed
+  qed
+  guess x
+    apply (rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
+    apply (rule compact_interval convex_interval)+ unfolding interior_closed_interval
+    apply (rule 1 2 3)+
+    done
+  note x=this
+  have "?F x \<noteq> 0"
+    apply (rule x0)
+    using x(1)
+    apply auto
+    done
+  then have *: "infnorm (sqprojection (?F x)) = 1"
+    unfolding o_def by (rule lem2[rule_format])
+  have nx: "infnorm x = 1"
+    apply (subst x(2)[THEN sym])
+    unfolding *[THEN sym] o_def
+    apply (rule lem1[rule_format])
+    done
+  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"
+    and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
+    apply -
+    apply (rule_tac[!] allI impI)+
+  proof -
+    fix x :: "real^2"
+    fix i :: 2
+    assume x: "x \<noteq> 0"
+    have "inverse (infnorm x) > 0"
+      using x[unfolded infnorm_pos_lt[THEN sym]] by auto
+    then show "(0 < sqprojection x $ i) = (0 < x $ i)"
+      and "(sqprojection x $ i < 0) = (x $ i < 0)"
       unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
-      unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
+      unfolding zero_less_mult_iff mult_less_0_iff
+      by (auto simp add: field_simps)
+  qed
   note lem3 = this[rule_format]
-  have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
-  hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
-  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto 
-  thus False proof- fix P Q R S 
-    presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
-  next assume as:"x$1 = 1"
-    hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
+  have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
+    using x(1) unfolding mem_interval_cart by auto
+  then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
+    unfolding right_minus_eq
+    apply -
+    apply (rule as)
+    apply auto
+    done
+  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1"
+    using nx unfolding infnorm_eq_1_2 by auto 
+  then show False
+  proof -
+    fix P Q R S 
+    presume "P \<or> Q \<or> R \<or> S"
+      and "P \<Longrightarrow> False"
+      and "Q \<Longrightarrow> False"
+      and "R \<Longrightarrow> False"
+      and "S \<Longrightarrow> False"
+    then show False by auto
+  next
+    assume as: "x$1 = 1"
+    then have *: "f (x $ 1) $ 1 = 1"
+      using assms(6) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-      apply(erule_tac x=1 in allE) by auto 
-  next assume as:"x$1 = -1"
-    hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "g (x $ 2) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(2)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
+      apply (erule_tac x=1 in allE)
+      apply auto
+      done
+  next
+    assume as: "x$1 = -1"
+    then have *: "f (x $ 1) $ 1 = - 1"
+      using assms(5) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-      apply(erule_tac x=1 in allE) by auto
-  next assume as:"x$2 = 1"
-    hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "g (x $ 2) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(2)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
+      apply (erule_tac x=1 in allE)
+      apply auto
+      done
+  next
+    assume as: "x$2 = 1"
+    then have *: "g (x $ 2) $ 2 = 1"
+      using assms(8) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-     apply(erule_tac x=2 in allE) by auto
- next assume as:"x$2 = -1"
-    hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "f (x $ 1) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(1)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      apply (erule_tac x=2 in allE)
+      apply auto
+      done
+  next
+    assume as: "x$2 = -1"
+    then have *: "g (x $ 2) $ 2 = - 1"
+      using assms(7) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-      apply(erule_tac x=2 in allE) by auto qed(auto) qed
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "f (x $ 1) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(1)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      apply (erule_tac x=2 in allE)
+      apply auto
+      done
+  qed auto
+qed
 
-lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
-  assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
-  "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1"  "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
-  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
+lemma fashoda_unit_path:
+  fixes f g :: "real \<Rightarrow> real^2"
+  assumes "path f"
+    and "path g"
+    and "path_image f \<subseteq> {- 1..1}"
+    and "path_image g \<subseteq> {- 1..1}"
+    and "(pathstart f)$1 = -1"
+    and "(pathfinish f)$1 = 1"
+    and "(pathstart g)$2 = -1"
+    and "(pathfinish g)$2 = 1"
+  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
+proof -
   note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
   def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
-  have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
-  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) 
+  have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
+    unfolding iscale_def by auto
+  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
+  proof (rule fashoda_unit)
     show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
       using isc and assms(3-4) unfolding image_compose by auto
-    have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
+    have *: "continuous_on {- 1..1} iscale"
+      unfolding iscale_def by (rule continuous_on_intros)+
     show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
-      apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
-      by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto
-    show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1"
-      unfolding o_def iscale_def using assms by(auto simp add:*) qed
+      apply -
+      apply (rule_tac[!] continuous_on_compose[OF *])
+      apply (rule_tac[!] continuous_on_subset[OF _ isc])
+      apply (rule assms)+
+      done
+    have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
+      unfolding vec_eq_iff by auto
+    show "(f \<circ> iscale) (- 1) $ 1 = - 1"
+      and "(f \<circ> iscale) 1 $ 1 = 1"
+      and "(g \<circ> iscale) (- 1) $ 2 = -1"
+      and "(g \<circ> iscale) 1 $ 2 = 1"
+      unfolding o_def iscale_def
+      using assms
+      by (auto simp add: *)
+  qed
   then guess s .. from this(2) guess t .. note st=this
-  show thesis apply(rule_tac z="f (iscale s)" in that)
-    using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
-    apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
-    using isc[unfolded subset_eq, rule_format] by auto qed
+  show thesis
+    apply (rule_tac z="f (iscale s)" in that)
+    using st `s\<in>{- 1..1}`
+    unfolding o_def path_image_def image_iff
+    apply -
+    apply (rule_tac x="iscale s" in bexI)
+    prefer 3
+    apply (rule_tac x="iscale t" in bexI)
+    using isc[unfolded subset_eq, rule_format]
+    apply auto
+    done
+qed
 
 lemma fashoda: fixes b::"real^2"
   assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
diff -r 773302e7741d -r fcd36f587512 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Isar/keyword.ML	Thu Sep 12 20:54:26 2013 +0200
@@ -23,6 +23,7 @@
   val thy_script: T
   val thy_goal: T
   val qed: T
+  val qed_script: T
   val qed_block: T
   val qed_global: T
   val prf_heading2: T
@@ -103,6 +104,7 @@
 val thy_script = kind "thy_script";
 val thy_goal = kind "thy_goal";
 val qed = kind "qed";
+val qed_script = kind "qed_script";
 val qed_block = kind "qed_block";
 val qed_global = kind "qed_global";
 val prf_heading2 = kind "prf_heading2";
@@ -121,7 +123,7 @@
 
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
+    thy_load, thy_decl, thy_script, thy_goal, qed, qed_script, qed_block, qed_global,
     prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
@@ -242,7 +244,7 @@
     thy_load, thy_decl, thy_script, thy_goal];
 
 val is_proof = command_category
-  [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
+  [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
     prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
     prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
@@ -252,7 +254,7 @@
 
 val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
-val is_qed = command_category [qed, qed_block];
+val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
 end;
diff -r 773302e7741d -r fcd36f587512 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Isar/keyword.scala	Thu Sep 12 20:54:26 2013 +0200
@@ -25,6 +25,7 @@
   val THY_SCRIPT = "thy_script"
   val THY_GOAL = "thy_goal"
   val QED = "qed"
+  val QED_SCRIPT = "qed_script"
   val QED_BLOCK = "qed_block"
   val QED_GLOBAL = "qed_global"
   val PRF_HEADING2 = "prf_heading2"
@@ -53,10 +54,12 @@
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
-    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, PRF_BLOCK,
-      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
+      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
+      PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   val proof1 =
-    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
+    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
+      PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
 }
diff -r 773302e7741d -r fcd36f587512 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Pure.thy	Thu Sep 12 20:54:26 2013 +0200
@@ -68,7 +68,8 @@
   and "}" :: prf_close % "proof"
   and "next" :: prf_block % "proof"
   and "qed" :: qed_block % "proof"
-  and "by" ".." "." "done" "sorry" :: "qed" % "proof"
+  and "by" ".." "." "sorry" :: "qed" % "proof"
+  and "done" :: "qed_script" % "proof"
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
   and "apply_end" :: prf_script % "proof" == ""
diff -r 773302e7741d -r fcd36f587512 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/System/gui_setup.scala	Thu Sep 12 20:54:26 2013 +0200
@@ -44,7 +44,7 @@
     // values
     text.append("JVM name: " + Platform.jvm_name + "\n")
     text.append("JVM platform: " + Platform.jvm_platform + "\n")
-    text.append("JVM home: " + java.lang.System.getProperty("java.home") + "\n")
+    text.append("JVM home: " + java.lang.System.getProperty("java.home", "") + "\n")
     try {
       Isabelle_System.init()
       if (Platform.is_windows)
diff -r 773302e7741d -r fcd36f587512 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Sep 12 20:54:26 2013 +0200
@@ -21,7 +21,7 @@
 
   def jdk_home(): String =
   {
-    val java_home = System.getProperty("java.home")
+    val java_home = System.getProperty("java.home", "")
     val home = new JFile(java_home)
     val parent = home.getParent
     if (home.getName == "jre" && parent != null &&
@@ -74,9 +74,9 @@
       set_cygwin_root()
       val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
 
-      val user_home = System.getProperty("user.home")
+      val user_home = System.getProperty("user.home", "")
       val env =
-        if (user_home == null || env0.isDefinedAt("HOME")) env0
+        if (user_home == "" || env0.isDefinedAt("HOME")) env0
         else env0 + ("HOME" -> user_home)
 
       val system_home =
@@ -84,8 +84,8 @@
         else
           env.get("ISABELLE_HOME") match {
             case None | Some("") =>
-              val path = System.getProperty("isabelle.home")
-              if (path == null || path == "") error("Unknown Isabelle home directory")
+              val path = System.getProperty("isabelle.home", "")
+              if (path == "") error("Unknown Isabelle home directory")
               else path
             case Some(path) => path
           }
diff -r 773302e7741d -r fcd36f587512 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/System/platform.scala	Thu Sep 12 20:54:26 2013 +0200
@@ -16,8 +16,8 @@
 {
   /* main OS variants */
 
-  val is_macos = System.getProperty("os.name") == "Mac OS X"
-  val is_windows = System.getProperty("os.name").startsWith("Windows")
+  val is_macos = System.getProperty("os.name", "") == "Mac OS X"
+  val is_windows = System.getProperty("os.name", "").startsWith("Windows")
 
 
   /* Platform identifiers */
@@ -35,7 +35,7 @@
   lazy val jvm_platform: String =
   {
     val arch =
-      System.getProperty("os.arch") match {
+      System.getProperty("os.arch", "") match {
         case X86() => "x86"
         case X86_64() => "x86_64"
         case Sparc() => "sparc"
@@ -43,7 +43,7 @@
         case _ => error("Failed to determine CPU architecture")
       }
     val os =
-      System.getProperty("os.name") match {
+      System.getProperty("os.name", "") match {
         case Solaris() => "solaris"
         case Linux() => "linux"
         case Darwin() => "darwin"
@@ -56,6 +56,6 @@
 
   /* JVM name */
 
-  val jvm_name: String = System.getProperty("java.vm.name")
+  val jvm_name: String = System.getProperty("java.vm.name", "")
 }
 
diff -r 773302e7741d -r fcd36f587512 src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/Tools/keywords.scala	Thu Sep 12 20:54:26 2013 +0200
@@ -27,6 +27,7 @@
     "thy_decl" -> "theory-decl",
     "thy_script" -> "theory-script",
     "thy_goal" -> "theory-goal",
+    "qed_script" -> "qed",
     "qed_block" -> "qed-block",
     "qed_global" -> "qed-global",
     "prf_heading2" -> "proof-heading",
diff -r 773302e7741d -r fcd36f587512 src/Pure/Tools/main.scala
diff -r 773302e7741d -r fcd36f587512 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Pure/build-jars	Thu Sep 12 20:54:26 2013 +0200
@@ -140,19 +140,10 @@
 [ "$#" -ne 0 ] && usage
 
 
-## dependencies
-
-declare -a JFREECHART_JARS=()
-for NAME in $JFREECHART_JAR_NAMES
-do
-  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
-done
-
-
 ## build
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/ext/Pure.jar"
+TARGET="$TARGET_DIR/Pure.jar"
 
 declare -a PIDE_SOURCES=()
 declare -a PURE_SOURCES=()
@@ -203,14 +194,10 @@
 
   SCALAC_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -d classes"
 
-  JFXRT="$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
-
   (
-    for X in "$JFXRT" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar" classes
-    do
-      CLASSPATH="$CLASSPATH:$X"
-    done
-    CLASSPATH="$(jvmpath "$CLASSPATH")"
+    classpath "$ISABELLE_JDK_HOME/jre/lib/jfxrt.jar"
+    classpath classes
+    export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
 
     if [ "$TEST_PIDE" = true ]; then
       isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" || \
@@ -223,7 +210,7 @@
     fi
   ) || exit "$?"
 
-  mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
+  mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
 
   pushd classes >/dev/null
 
@@ -238,13 +225,10 @@
 
   cp "$SCALA_HOME/lib/scala-compiler.jar" \
     "$SCALA_HOME/lib/scala-library.jar" \
-    "$SCALA_HOME/lib/scala-swing.jar" "$TARGET_DIR/ext"
-
-  [ -e "$SCALA_HOME/lib/scala-actors.jar" ] && \
-    cp "$SCALA_HOME/lib/scala-actors.jar" "$TARGET_DIR/ext"
-
-  [ -e "$SCALA_HOME/lib/scala-reflect.jar" ] && \
-    cp "$SCALA_HOME/lib/scala-reflect.jar" "$TARGET_DIR/ext"
+    "$SCALA_HOME/lib/scala-swing.jar" \
+    "$SCALA_HOME/lib/scala-actors.jar" \
+    "$SCALA_HOME/lib/scala-reflect.jar" \
+    "$TARGET_DIR"
 
   popd >/dev/null
 
diff -r 773302e7741d -r fcd36f587512 src/Tools/Graphview/lib/Tools/graphview
--- a/src/Tools/Graphview/lib/Tools/graphview	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview	Thu Sep 12 20:54:26 2013 +0200
@@ -94,10 +94,10 @@
 
 pushd "$GRAPHVIEW_HOME" >/dev/null || failed
 
-PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
+PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
-TARGET="$TARGET_DIR/ext/Graphview.jar"
+TARGET="$TARGET_DIR/Graphview.jar"
 
 declare -a UPDATED=()
 
@@ -139,12 +139,12 @@
   rm -rf classes && mkdir classes
 
   (
-    #workaround for scalac
+    #workaround for scalac 2.10.2
     function stty() { :; }
     export -f stty
 
-    CLASSPATH="$CLASSPATH:$PURE_JAR"
-    CLASSPATH="$(jvmpath "$CLASSPATH")"
+    classpath "$PURE_JAR"
+    export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
     exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}"
   ) || fail "Failed to compile sources"
 
diff -r 773302e7741d -r fcd36f587512 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 12 20:54:26 2013 +0200
@@ -198,8 +198,8 @@
   fi
 fi
 
-PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
-GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"
+PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
+GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/Graphview.jar"
 
 pushd "$JEDIT_HOME" >/dev/null || failed
 
@@ -216,12 +216,6 @@
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
 )
 
-declare -a JFREECHART_JARS=()
-for NAME in $JFREECHART_JAR_NAMES
-do
-  JFREECHART_JARS["${#JFREECHART_JARS[@]}"]="$JFREECHART_HOME/lib/$NAME"
-done
-
 
 # target
 
@@ -238,8 +232,8 @@
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
       declare -a DEPS=(
-        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar"
-        "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
+        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
+        "${SOURCES[@]}" "${RESOURCES[@]}"
       )
     elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
       declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
@@ -293,16 +287,15 @@
 
   cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
   (
-    #workaround for scalac
+    #workaround for scalac 2.10.2
     function stty() { :; }
     export -f stty
 
-    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" \
-      "$XZ_JAVA_HOME/lib/xz.jar" "$PURE_JAR" "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
+    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR"
     do
-      CLASSPATH="$CLASSPATH:$JAR"
+      classpath "$JAR"
     done
-    CLASSPATH="$(jvmpath "$CLASSPATH")"
+    export CLASSPATH="$(jvmpath "$ISABELLE_CLASSPATH")"
     exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d dist/classes "${SOURCES[@]}"
   ) || fail "Failed to compile sources"
 
@@ -317,9 +310,9 @@
 
 ## main
 
-if [ "$BUILD_ONLY" = false ]; then
+if [ "$BUILD_ONLY" = false ]
+then
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
-
-  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
-    -classpath "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" isabelle.Main "${ARGS[@]}"
+  classpath "$JEDIT_HOME/dist/jedit.jar"
+  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
 fi
diff -r 773302e7741d -r fcd36f587512 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Sep 12 20:54:26 2013 +0200
@@ -75,6 +75,7 @@
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
       Keyword.THY_SCRIPT -> LABEL,
+      Keyword.QED_SCRIPT -> DIGIT,
       Keyword.PRF_SCRIPT -> DIGIT,
       Keyword.PRF_ASM -> KEYWORD3,
       Keyword.PRF_ASM_GOAL -> KEYWORD3,
diff -r 773302e7741d -r fcd36f587512 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Thu Sep 12 17:36:06 2013 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Thu Sep 12 20:54:26 2013 +0200
@@ -46,7 +46,14 @@
         find_files(new JFile(start),
           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
       else Nil
-    val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
+
+    val initial_class_path =
+      Library.space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+
+    val path =
+      initial_class_path :::
+      find_jars(jEdit.getSettingsDirectory) :::
+      find_jars(jEdit.getJEditHome)
     path.mkString(JFile.pathSeparator)
   }