# HG changeset patch
# User wenzelm
# Date 1459720652 -7200
# Node ID 388719339ada7fe43336dc42b654c5bac3fb7303
# Parent  609f97d79bc282c710c071df90c650eff59857d0# Parent  d9744f41a4eca4dc7b9849ea90ec5ffa5341d392
merged

diff -r 609f97d79bc2 -r 388719339ada Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: build Isabelle documentation
-
-isabelle_admin_build jars || exit $?
-
-
-case "$ISABELLE_JAVA_PLATFORM" in
-  x86-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
-    ;;
-  x86_64-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
-    ;;
-esac
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-isabelle java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
diff -r 609f97d79bc2 -r 388719339ada NEWS
--- a/NEWS	Sun Apr 03 10:25:17 2016 +0200
+++ b/NEWS	Sun Apr 03 23:57:32 2016 +0200
@@ -259,6 +259,12 @@
 
 *** System ***
 
+* Many Isabelle tools that require a Java runtime system refer to the
+settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
+depending on the underlying platform. The settings for "isabelle build"
+ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
+discontinued. Potential INCOMPATIBILITY.
+
 * The Isabelle system environment always ensures that the main
 executables are found within the shell search $PATH: "isabelle" and
 "isabelle_scala_script".
diff -r 609f97d79bc2 -r 388719339ada bin/isabelle
--- a/bin/isabelle	Sun Apr 03 10:25:17 2016 +0200
+++ b/bin/isabelle	Sun Apr 03 23:57:32 2016 +0200
@@ -18,46 +18,40 @@
 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
 
-## diagnostics
+## external tool (shell script)
+
+if [ "$#" -ge 1 -a "$1" != "-?" ]
+then
+  TOOL_NAME="$1"
 
-function usage()
-{
-  echo
-  echo "Usage: $PRG NAME [ARGS ...]"
-  echo
-  echo "  Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
-  echo
-  echo "Available tools:"
-  perl -w "$ISABELLE_HOME/lib/scripts/tools.pl"
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
+  splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
+  for DIR in "${TOOLS[@]}"
+  do
+    TOOL="$DIR/$TOOL_NAME"
+    case "$TOOL" in
+      *~ | *.orig) ;;
+      *)
+        if [ -f "$TOOL" -a -x "$TOOL" ]; then
+          shift
+          exec "$TOOL" "$@"
+        fi
+        ;;
+    esac
+  done
+fi
 
 
-## args
-
-[ "$#" -lt 1 -o "$1" = "-?" ] && usage
+## internal tool or usage (Scala)
 
-TOOLNAME="$1"
-shift
-
-
-## main
+isabelle_admin_build jars || exit $?
 
-splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
+case "$ISABELLE_JAVA_PLATFORM" in
+  x86-*)
+    eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS32)"
+    ;;
+  x86_64-*)
+    eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS64)"
+    ;;
+esac
 
-for DIR in "${TOOLS[@]}"
-do
-  TOOL="$DIR/$TOOLNAME"
-  case "$TOOL" in
-    *~ | *.orig) ;;
-    *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;;
-  esac
-done
-
-fail "Unknown Isabelle tool: $TOOLNAME"
+exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@"
diff -r 609f97d79bc2 -r 388719339ada etc/settings
--- a/etc/settings	Sun Apr 03 10:25:17 2016 +0200
+++ b/etc/settings	Sun Apr 03 23:57:32 2016 +0200
@@ -16,6 +16,9 @@
 
 ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0"
 
+ISABELLE_TOOL_JAVA_OPTIONS32="-Djava.awt.headless=true -Xms128m -Xmx1024m -Xss1m"
+ISABELLE_TOOL_JAVA_OPTIONS64="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"
+
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
 #paranoia settings -- avoid intrusion of alien options
@@ -39,9 +42,6 @@
 
 ISABELLE_BUILD_OPTIONS=""
 
-ISABELLE_BUILD_JAVA_OPTIONS32="-Djava.awt.headless=true -Xms128m -Xmx1024m -Xss1m"
-ISABELLE_BUILD_JAVA_OPTIONS64="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"
-
 
 ###
 ### Document preparation (cf. isabelle latex/document)
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/build
--- a/lib/Tools/build	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: build and manage Isabelle sessions
-
-isabelle_admin_build jars || exit $?
-
-case "$ISABELLE_JAVA_PLATFORM" in
-  x86-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
-    ;;
-  x86_64-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
-    ;;
-esac
-
-eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-exec isabelle java "${JAVA_ARGS[@]}" isabelle.Build "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/check_sources
--- a/lib/Tools/check_sources	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: some sanity checks for Isabelle sources
-
-isabelle_admin_build jars || exit $?
-
-isabelle java isabelle.Check_Sources "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/console
--- a/lib/Tools/console	Sun Apr 03 10:25:17 2016 +0200
+++ b/lib/Tools/console	Sun Apr 03 23:57:32 2016 +0200
@@ -8,14 +8,14 @@
 
 case "$ISABELLE_JAVA_PLATFORM" in
   x86-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
+    ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS32"
     ;;
   x86_64-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
+    ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS64"
     ;;
 esac
 
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
 
 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
 
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/doc
--- a/lib/Tools/doc	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: view Isabelle documentation
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Doc "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/getenv
--- a/lib/Tools/getenv	Sun Apr 03 10:25:17 2016 +0200
+++ b/lib/Tools/getenv	Sun Apr 03 23:57:32 2016 +0200
@@ -57,6 +57,7 @@
 
 # args
 
+[ -z "$ALL" -a -z "$DUMP" -a "$#" -eq 0 ] && usage
 [ -n "$ALL" -a "$#" -ne 0 ] && usage
 
 
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/options
--- a/lib/Tools/options	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: print Isabelle system options
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Options "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/process
--- a/lib/Tools/process	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: raw ML process (batch mode)
-
-isabelle_admin_build jars || exit $?
-
-case "$ISABELLE_JAVA_PLATFORM" in
-  x86-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
-    ;;
-  x86_64-*)
-    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
-    ;;
-esac
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-
-exec isabelle java isabelle.ML_Process "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/update_cartouches
--- a/lib/Tools/update_cartouches	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update theory syntax to use cartouches
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Cartouches "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/update_header
--- a/lib/Tools/update_header	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: replace obsolete theory header command
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Header "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/update_then
--- a/lib/Tools/update_then	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Then "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/Tools/update_theorems
--- a/lib/Tools/update_theorems	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update toplevel theorem keywords
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Theorems "$@"
diff -r 609f97d79bc2 -r 388719339ada lib/scripts/tools.pl
--- a/lib/scripts/tools.pl	Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-#
-# Author: Makarius
-#
-# tools.pl - list Isabelle tools with description
-#
-
-use strict;
-use warnings;
-
-my @tools = ();
-
-for my $dir (split(":", $ENV{"ISABELLE_TOOLS"})) {
-  if (-d $dir) {
-    if (opendir DIR, $dir) {
-      for my $name (readdir DIR) {
-        my $file = "$dir/$name";
-        if (-f $file and -x $file and !($file =~ /~$/ or $file =~ /\.orig$/)) {
-          if (open FILE, $file) {
-            my $description;
-            while (<FILE>) {
-              if (!defined($description) and m/DESCRIPTION: *(.*)$/) {
-                $description = $1;
-              }
-            }
-            close FILE;
-            if (defined($description)) {
-              push(@tools, "  $name - $description\n");
-            }
-          }
-        }
-      }
-      closedir DIR;
-    }
-  }
-}
-
-for (sort @tools) { print };
diff -r 609f97d79bc2 -r 388719339ada src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Doc/System/Environment.thy	Sun Apr 03 23:57:32 2016 +0200
@@ -267,7 +267,7 @@
   @{verbatim [display]
 \<open>Usage: isabelle TOOL [ARGS ...]
 
-  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
 
 Available tools:
   ...\<close>}
diff -r 609f97d79bc2 -r 388719339ada src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Doc/System/Sessions.thy	Sun Apr 03 23:57:32 2016 +0200
@@ -270,7 +270,6 @@
   Build and manage Isabelle sessions, depending on implicit settings:
 
   ISABELLE_BUILD_OPTIONS="..."
-  ISABELLE_BUILD_JAVA_OPTIONS="..."
 
   ML_PLATFORM="..."
   ML_HOME="..."
diff -r 609f97d79bc2 -r 388719339ada src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Doc/antiquote_setup.ML	Sun Apr 03 23:57:32 2016 +0200
@@ -157,17 +157,6 @@
   (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
     handle ERROR _ => false;
 
-fun check_tool ctxt (name, pos) =
-  let
-    fun tool dir =
-      let val path = Path.append dir (Path.basic name)
-      in if File.exists path then SOME path else NONE end;
-  in
-    (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
-      NONE => false
-    | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
-  end;
-
 val arg = enclose "{" "}" o clean_string;
 
 fun entity check markup binding index =
@@ -220,7 +209,7 @@
     entity_antiqs check_system_option "isasystem" @{binding system_option} #>
     entity_antiqs no_check "" @{binding inference} #>
     entity_antiqs no_check "isasystem" @{binding executable} #>
-    entity_antiqs check_tool "isatool" @{binding tool} #>
+    entity_antiqs no_check "isatool" @{binding tool} #>
     entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
     entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
 
diff -r 609f97d79bc2 -r 388719339ada src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Sun Apr 03 23:57:32 2016 +0200
@@ -2,7 +2,7 @@
     Author:     Andreas Lochbihler, ETH Zurich
 *)
 
-section {* Formalisation of chain-complete partial orders, continuity and admissibility *}
+section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
 
 theory Complete_Partial_Order2 imports 
   Main
@@ -83,10 +83,10 @@
     fix x'
     assume "x' \<in> (\<lambda>f. f x) ` Y"
     then obtain f where "f \<in> Y" "x' = f x" by blast
-    note `x' = f x` also
-    from `f \<in> Y` `x \<sqsubseteq> y` have "f x \<le> f y" by(blast dest: mono monotoneD)
+    note \<open>x' = f x\<close> also
+    from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD)
     also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''
-      by(rule ccpo_Sup_upper)(simp add: `f \<in> Y`)
+      by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>)
     finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .
   qed
 qed
@@ -108,9 +108,9 @@
   fix x'
   assume "x' \<in> f x ` Y"
   then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
-  also from mono1[OF `y' \<in> Y`] le have "\<dots> \<le> f y y'" by(rule monotoneD)
+  also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD)
   also have "\<dots> \<le> ?rhs" using chain'[OF y]
-    by (auto intro!: ccpo_Sup_upper simp add: `y' \<in> Y`)
+    by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>)
   finally show "x' \<le> ?rhs" .
 qed(rule x)
 
@@ -128,17 +128,17 @@
     fix x'
     assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"
     then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
-    also have "\<dots> \<le> ?rhs" using chain2[OF `y' \<in> Y`]
+    also have "\<dots> \<le> ?rhs" using chain2[OF \<open>y' \<in> Y\<close>]
     proof(rule ccpo_Sup_least)
       fix x
       assume "x \<in> f y' ` Y"
       then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
       def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y"
-      from chain `y \<in> Y` `y' \<in> Y` have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
-      hence "f y' y \<le> f y'' y''" using `y \<in> Y` `y' \<in> Y`
+      from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
+      hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close>
         by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
-      also from `y \<in> Y` `y' \<in> Y` have "y'' \<in> Y" by(simp add: y''_def)
-      from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \<in> Y`)
+      also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def)
+      from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: \<open>y'' \<in> Y\<close>)
       finally show "x \<le> ?rhs" by(simp add: x)
     qed
     finally show "x' \<le> ?rhs" .
@@ -149,9 +149,9 @@
     fix y
     assume "y \<in> (\<lambda>x. f x x) ` Y"
     then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
-    also from chain2[OF `x \<in> Y`] have "\<dots> \<le> \<Squnion>(f x ` Y)"
-      by(rule ccpo_Sup_upper)(simp add: `x \<in> Y`)
-    also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \<in> Y`)
+    also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
+      by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
+    also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
     finally show "y \<le> ?lhs" .
   qed
 qed
@@ -171,8 +171,8 @@
   fix x
   assume "x \<in> f ` Y"
   then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)
-  also have "y \<sqsubseteq> \<Or>Y" using ccpo chain `y \<in> Y` by(rule ccpo.ccpo_Sup_upper)
-  hence "f y \<le> f (\<Or>Y)" using `y \<in> Y` by(rule mono)
+  also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper)
+  hence "f y \<le> f (\<Or>Y)" using \<open>y \<in> Y\<close> by(rule mono)
   finally show "x \<le> \<dots>" .
 qed
 
@@ -196,14 +196,14 @@
     fix f g
     assume "f \<in> Z" "g \<in> Z"
       and "fun_ord op \<le> f g"
-    from chain1[OF `f \<in> Z`] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
+    from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
     proof(rule ccpo_Sup_least)
       fix x
       assume "x \<in> f ` Y"
       then obtain y where "y \<in> Y" "x = f y" by blast note this(2)
-      also have "\<dots> \<le> g y" using `fun_ord op \<le> f g` by(simp add: fun_ord_def)
-      also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF `g \<in> Z`]
-        by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+      also have "\<dots> \<le> g y" using \<open>fun_ord op \<le> f g\<close> by(simp add: fun_ord_def)
+      also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF \<open>g \<in> Z\<close>]
+        by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
       finally show "x \<le> \<Squnion>(g ` Y)" .
     qed
   qed
@@ -219,9 +219,9 @@
       fix x'
       assume "x' \<in> (\<lambda>f. f x) ` Z"
       then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
-      also have "f x \<le> f y" using `f \<in> Z` `x \<sqsubseteq> y` by(rule monotoneD[OF mono])
+      also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
       also have "f y \<le> ?rhs" using chain3
-        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
+        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
       finally show "x' \<le> ?rhs" .
     qed
   qed
@@ -231,14 +231,14 @@
     fix x
     assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"
     then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)
-    also have "\<dots> \<le> ?rhs" using chain1[OF `f \<in> Z`]
+    also have "\<dots> \<le> ?rhs" using chain1[OF \<open>f \<in> Z\<close>]
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> f ` Y"
       then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
       also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
-        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
-      also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
+      also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
       finally show "x' \<le> ?rhs" .
     qed
     finally show "x \<le> ?rhs" .
@@ -254,10 +254,10 @@
       fix x'
       assume "x' \<in> (\<lambda>f. f y) ` Z"
       then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
-      also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF `f \<in> Z`]
-        by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+      also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
+        by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
       also have "\<dots> \<le> ?lhs" using chain2
-        by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
+        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
       finally show "x' \<le> ?lhs" .
     qed
     finally show "x \<le> ?lhs" .
@@ -314,9 +314,9 @@
     assume "x' \<in> (\<lambda>f. f x) ` ?iter"
     then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
     also have "f x \<le> f y"
-      by(rule monotoneD[OF iterates_mono[OF `f \<in> ?iter` mono2]])(blast intro: `x \<sqsubseteq> y`)+
+      by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+
     also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
-      by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
+      by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
     finally show "x' \<le> \<dots>" .
   qed
 qed
@@ -333,7 +333,7 @@
   shows "monotone orda ordc (\<lambda>x. f x (t x))"
 by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
 
-subsection {* Continuity *}
+subsection \<open>Continuity\<close>
 
 definition cont :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
 where
@@ -345,10 +345,10 @@
   "mcont luba orda lubb ordb f \<longleftrightarrow>
    monotone orda ordb f \<and> cont luba orda lubb ordb f"
 
-subsubsection {* Theorem collection @{text cont_intro} *}
+subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close>
 
 named_theorems cont_intro "continuity and admissibility intro rules"
-ML {*
+ML \<open>
 (* apply cont_intro rules as intro and try to solve 
    the remaining of the emerging subgoals with simp *)
 fun cont_intro_tac ctxt =
@@ -374,13 +374,13 @@
   end
   handle THM _ => NONE 
   | TYPE _ => NONE
-*}
+\<close>
 
 simproc_setup "cont_intro"
   ( "ccpo.admissible lub ord P"
   | "mcont lub ord lub' ord' f"
   | "monotone ord ord' f"
-  ) = {* K cont_intro_simproc *}
+  ) = \<open>K cont_intro_simproc\<close>
 
 lemmas [cont_intro] =
   call_mono
@@ -604,10 +604,10 @@
       fix x'
       assume "x' \<in> (\<lambda>f. f x) ` ?iter"
       then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
-      also from _ `x \<sqsubseteq> y` have "f x \<le> f y"
-        by(rule mcont_monoD[OF iterates_mcont[OF `f \<in> ?iter` mcont]])
+      also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
+        by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
       also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
-        by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
+        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
       finally show "x' \<le> \<dots>" .
     qed
   next
@@ -783,7 +783,7 @@
 
 end
 
-subsection {* Admissibility *}
+subsection \<open>Admissibility\<close>
 
 lemma admissible_subst:
   assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)"
@@ -860,10 +860,10 @@
     fix x
     assume "x \<in> f ` A"
     then obtain y where "y \<in> A" "x = f y" by blast note this(2)
-    also have "f y \<le> g y" using le `y \<in> A` by simp
+    also have "f y \<le> g y" using le \<open>y \<in> A\<close> by simp
     also have "Complete_Partial_Order.chain op \<le> (g ` A)"
       using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
-    hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \<in> A`)
+    hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> A\<close>)
     finally show "x \<le> \<dots>" .
   qed
   also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
@@ -992,7 +992,7 @@
 
 end
 
-subsection {* @{term "op ="} as order *}
+subsection \<open>@{term "op ="} as order\<close>
 
 definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
 where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
@@ -1038,7 +1038,7 @@
   \<Longrightarrow> mcont the_Sup op = lub ord f"
 by(simp add: mcont_def cont_eqI monotone_eqI)
 
-subsection {* ccpo for products *}
+subsection \<open>ccpo for products\<close>
 
 definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
 where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
@@ -1197,7 +1197,7 @@
   with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
   moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto
   ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba
-    by(simp add: prod_lub_def `Y \<noteq> {}` lub_singleton_def)
+    by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def)
 qed
 
 lemma cont_prodD2: 
@@ -1253,9 +1253,9 @@
   have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))"
     by(simp add: prod_lub_def)
   also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y)"
-    by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] `Y \<noteq> {}`)
+    by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] \<open>Y \<noteq> {}\<close>)
   also from cont1 have "\<And>x. f (x, lubb (snd ` Y)) = \<Squnion>((\<lambda>y. f (x, y)) ` snd ` Y)"
-    by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] `Y \<noteq> {}`)
+    by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] \<open>Y \<noteq> {}\<close>)
   hence "\<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y) = \<Squnion>((\<lambda>x. \<dots> x) ` fst ` Y)" by simp
   also have "\<dots> = \<Squnion>((\<lambda>x. f (fst x, snd x)) ` Y)"
     unfolding image_image split_def using chain
@@ -1330,7 +1330,7 @@
   shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
 by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
 
-subsection {* Complete lattices as ccpo *}
+subsection \<open>Complete lattices as ccpo\<close>
 
 context complete_lattice begin
 
@@ -1374,8 +1374,8 @@
   fix y
   assume "y \<in> op \<squnion> x ` Y"
   then obtain z where "y = x \<squnion> z" and "z \<in> Y" by blast
-  from `z \<in> Y` have "z \<le> \<Squnion>Y" by(rule Sup_upper)
-  with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding `y = x \<squnion> z` by(rule sup_mono) simp
+  from \<open>z \<in> Y\<close> have "z \<le> \<Squnion>Y" by(rule Sup_upper)
+  with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding \<open>y = x \<squnion> z\<close> by(rule sup_mono) simp
 next
   fix y
   assume upper: "\<And>z. z \<in> op \<squnion> x ` Y \<Longrightarrow> z \<le> y"
@@ -1385,8 +1385,8 @@
     assume "z \<in> insert x Y"
     from assms obtain z' where "z' \<in> Y" by blast
     let ?z = "if z \<in> Y then x \<squnion> z else x \<squnion> z'"
-    have "z \<le> x \<squnion> ?z" using `z' \<in> Y` `z \<in> insert x Y` by auto
-    also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: `z' \<in> Y`)
+    have "z \<le> x \<squnion> ?z" using \<open>z' \<in> Y\<close> \<open>z \<in> insert x Y\<close> by auto
+    also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: \<open>z' \<in> Y\<close>)
     finally show "z \<le> y" .
   qed
 qed
@@ -1426,14 +1426,14 @@
 interpretation lfp: partial_function_definitions "op \<le> :: _ :: complete_lattice \<Rightarrow> _" Sup
 by(rule complete_lattice_partial_function_definitions)
 
-declaration {* Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
-  @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE *}
+declaration \<open>Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
+  @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
 
 interpretation gfp: partial_function_definitions "op \<ge> :: _ :: complete_lattice \<Rightarrow> _" Inf
 by(rule complete_lattice_partial_function_definitions_dual)
 
-declaration {* Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
-  @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE *}
+declaration \<open>Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
+  @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
 
 lemma insert_mono [partial_function_mono]:
    "monotone (fun_ord op \<subseteq>) op \<subseteq> A \<Longrightarrow> monotone (fun_ord op \<subseteq>) op \<subseteq> (\<lambda>y. insert x (A y))"
@@ -1505,23 +1505,23 @@
         fix u
         assume "u \<in> (\<lambda>x. g x z) ` Y"
         then obtain y' where "u = g y' z" "y' \<in> Y" by auto
-        from chain `y \<in> Y` `y' \<in> Y` have "ord y y' \<or> ord y' y" by(rule chainD)
+        from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "ord y y' \<or> ord y' y" by(rule chainD)
         thus "u \<le> ?rhs"
         proof
-          note `u = g y' z` also
+          note \<open>u = g y' z\<close> also
           assume "ord y y'"
           with f have "f y \<subseteq> f y'" by(rule mcont_monoD)
-          with `z \<in> f y`
+          with \<open>z \<in> f y\<close>
           have "g y' z \<le> \<Squnion>(g y' ` f y')" by(auto intro: Sup_upper)
-          also have "\<dots> \<le> ?rhs" using `y' \<in> Y` by(auto intro: Sup_upper)
+          also have "\<dots> \<le> ?rhs" using \<open>y' \<in> Y\<close> by(auto intro: Sup_upper)
           finally show ?thesis .
         next
-          note `u = g y' z` also
+          note \<open>u = g y' z\<close> also
           assume "ord y' y"
           with g have "g y' z \<le> g y z" by(rule mcont_monoD)
-          also have "\<dots> \<le> \<Squnion>(g y ` f y)" using `z \<in> f y`
+          also have "\<dots> \<le> \<Squnion>(g y ` f y)" using \<open>z \<in> f y\<close>
             by(auto intro: Sup_upper)
-          also have "\<dots> \<le> ?rhs" using `y \<in> Y` by(auto intro: Sup_upper)
+          also have "\<dots> \<le> ?rhs" using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
           finally show ?thesis .
         qed
       qed
@@ -1537,11 +1537,11 @@
         fix u
         assume "u \<in> g y ` f y"
         then obtain z where "u = g y z" "z \<in> f y" by auto
-        note `u = g y z`
+        note \<open>u = g y z\<close>
         also have "g y z \<le> \<Squnion>((\<lambda>x. g x z) ` Y)"
-          using `y \<in> Y` by(auto intro: Sup_upper)
+          using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
         also have "\<dots> = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y])
-        also have "\<dots> \<le> ?lhs" using `z \<in> f y` `y \<in> Y`
+        also have "\<dots> \<le> ?lhs" using \<open>z \<in> f y\<close> \<open>y \<in> Y\<close>
           by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y])
         finally show "u \<le> ?lhs" .
       qed
@@ -1567,7 +1567,7 @@
   shows admissible_Bex: "ccpo.admissible Union op \<subseteq> (\<lambda>A. \<exists>x\<in>A. P x)"
 by(rule ccpo.admissibleI)(auto)
 
-subsection {* Parallel fixpoint induction *}
+subsection \<open>Parallel fixpoint induction\<close>
 
 context
   fixes luba :: "'a set \<Rightarrow> 'a"
diff -r 609f97d79bc2 -r 388719339ada src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Apr 03 23:57:32 2016 +0200
@@ -443,7 +443,7 @@
 
 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
   by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
-  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
 lemma mset_less_eqI:
   "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
@@ -464,7 +464,7 @@
   by standard (simp, fact mset_le_exists_conv)
 
 declare subset_mset.zero_order[simp del]
-  -- \<open>this removes some simp rules not in the usual order for multisets\<close>
+  \<comment> \<open>this removes some simp rules not in the usual order for multisets\<close>
 
 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
    by (fact subset_mset.add_le_cancel_right)
@@ -587,7 +587,7 @@
   show "class.semilattice_inf op #\<inter> op \<subseteq># op \<subset>#"
     by standard (auto simp add: multiset_inter_def subseteq_mset_def)
 qed
-  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
 lemma multiset_inter_count [simp]:
   fixes A B :: "'a multiset"
@@ -712,7 +712,7 @@
 subsubsection \<open>Bounded union\<close>
 
 definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)
-  where "sup_subset_mset A B = A + (B - A)" -- \<open>FIXME irregular fact name\<close>
+  where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
 
 interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
 proof -
@@ -721,9 +721,9 @@
   show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#"
     by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
 qed
-  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
-
-lemma sup_subset_mset_count [simp]: -- \<open>FIXME irregular fact name\<close>
+  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+
+lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close>
   "count (A #\<union> B) x = max (count A x) (count B x)"
   by (simp add: sup_subset_mset_def)
 
@@ -1554,8 +1554,8 @@
   "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
 
 abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
-  where "\<Union># MM \<equiv> msetsum MM" -- \<open>FIXME ambiguous notation --
-    could likewise refer to @{text "\<Squnion>#"}\<close>
+  where "\<Union># MM \<equiv> msetsum MM" \<comment> \<open>FIXME ambiguous notation --
+    could likewise refer to \<open>\<Squnion>#\<close>\<close>
 
 lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
   by (induct MM) auto
@@ -2115,7 +2115,7 @@
     unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
   show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
     by standard (auto simp add: le_multiset_def irrefl dest: trans)
-qed -- \<open>FIXME avoid junk stemming from type class interpretation\<close>
+qed \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
 
 lemma mult_less_irrefl [elim!]:
   fixes M :: "'a::order multiset"
diff -r 609f97d79bc2 -r 388719339ada src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Sun Apr 03 23:57:32 2016 +0200
@@ -606,10 +606,10 @@
     shows "valid_path (f o g)"
 proof -
   obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1} - s"
-    using `valid_path g` unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
+    using \<open>valid_path g\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
   have "f \<circ> g differentiable at t" when "t\<in>{0..1} - s" for t
     proof (rule differentiable_chain_at)
-      show "g differentiable at t" using `valid_path g`
+      show "g differentiable at t" using \<open>valid_path g\<close>
         by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
     next
       have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
@@ -627,7 +627,7 @@
     next
       have "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
         using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
-          `valid_path g` piecewise_C1_differentiable_on_def valid_path_def
+          \<open>valid_path g\<close> piecewise_C1_differentiable_on_def valid_path_def
         by blast
       then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
         using continuous_on_subset by blast
@@ -650,14 +650,14 @@
       have "isCont f x" when "x\<in>path_image g" for x
         proof -
           obtain f' where "(f has_field_derivative f') (at x)"
-            using der[rule_format] `x\<in>path_image g` by auto
+            using der[rule_format] \<open>x\<in>path_image g\<close> by auto
           thus ?thesis using DERIV_isCont by auto
         qed
       then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
-      then show ?thesis using path_continuous_image `valid_path g` valid_path_imp_path by auto
+      then show ?thesis using path_continuous_image \<open>valid_path g\<close> valid_path_imp_path by auto
     qed
   ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
-    using `finite s` by auto
+    using \<open>finite s\<close> by auto
 qed
 
 
@@ -5730,13 +5730,13 @@
 lemma valid_path_compose_holomorphic:
   assumes "valid_path g" and holo:"f holomorphic_on s" and "open s" "path_image g \<subseteq> s"
   shows "valid_path (f o g)"
-proof (rule valid_path_compose[OF `valid_path g`])
+proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
   fix x assume "x \<in> path_image g"
   then show "\<exists>f'. (f has_field_derivative f') (at x)"
-    using holo holomorphic_on_open[OF `open s`] `path_image g \<subseteq> s` by auto
+    using holo holomorphic_on_open[OF \<open>open s\<close>] \<open>path_image g \<subseteq> s\<close> by auto
 next
   have "deriv f holomorphic_on s"
-    using holomorphic_deriv holo `open s` by auto
+    using holomorphic_deriv holo \<open>open s\<close> by auto
   then show "continuous_on (path_image g) (deriv f)"
     using assms(4) holomorphic_on_imp_continuous_on holomorphic_on_subset by auto
 qed
diff -r 609f97d79bc2 -r 388719339ada src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Sun Apr 03 23:57:32 2016 +0200
@@ -964,7 +964,7 @@
     proof -
       have f0: "(f \<longlongrightarrow> 0) at_infinity"
       proof -
-        have DIM_complex[intro]: "2 \<le> DIM(complex)"  --\<open>should not be necessary!\<close>
+        have DIM_complex[intro]: "2 \<le> DIM(complex)"  \<comment>\<open>should not be necessary!\<close>
           by simp
         have "continuous_on (inverse ` (ball 0 r - {0})) f"
           using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast
@@ -2149,61 +2149,61 @@
     proof -
       assume "n>m"
       have "(h \<longlongrightarrow> 0) (at z within ball z r)" 
-        proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (n - m) * g w"]) 
-          have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using `n>m` asm
+        proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (n - m) * g w"]) 
+          have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using \<open>n>m\<close> asm
             by (auto simp add:field_simps power_diff)
           then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> 
             \<Longrightarrow> (x' - z) ^ (n - m) * g x' = h x'" for x' by auto
         next
           def F\<equiv>"at z within ball z r"
             and f'\<equiv>"\<lambda>x. (x - z) ^ (n-m)"
-          have "f' z=0" using `n>m` unfolding f'_def by auto
+          have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
           moreover have "continuous F f'" unfolding f'_def F_def
             by (intro continuous_intros)
           ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
             by (simp add: continuous_within)            
           moreover have "(g \<longlongrightarrow> g z) F"
-            using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] `r>0`
+            using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \<open>r>0\<close>
             unfolding F_def by auto
           ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
         qed
       moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)" 
         using holomorphic_on_imp_continuous_on[OF h_holo] 
-        by (auto simp add:continuous_on_def `r>0`) 
-      moreover have "at z within ball z r \<noteq> bot" using `r>0` 
+        by (auto simp add:continuous_on_def \<open>r>0\<close>) 
+      moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> 
         by (auto simp add:trivial_limit_within islimpt_ball)
       ultimately have "h z=0" by (auto intro: tendsto_unique)
-      thus False using asm `r>0` by auto
+      thus False using asm \<open>r>0\<close> by auto
     qed
   moreover have "m>n \<Longrightarrow> False"
     proof -
       assume "m>n"
       have "(g \<longlongrightarrow> 0) (at z within ball z r)" 
-        proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (m - n) * h w"]) 
-          have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using `m>n` asm
+        proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (m - n) * h w"]) 
+          have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using \<open>m>n\<close> asm
             by (auto simp add:field_simps power_diff)
           then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> 
             \<Longrightarrow> (x' - z) ^ (m - n) * h x' = g x'" for x' by auto
         next
           def F\<equiv>"at z within ball z r"
             and f'\<equiv>"\<lambda>x. (x - z) ^ (m-n)"
-          have "f' z=0" using `m>n` unfolding f'_def by auto
+          have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
           moreover have "continuous F f'" unfolding f'_def F_def
             by (intro continuous_intros)
           ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
             by (simp add: continuous_within)            
           moreover have "(h \<longlongrightarrow> h z) F"
-            using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] `r>0`
+            using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \<open>r>0\<close>
             unfolding F_def by auto
           ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
         qed
       moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)" 
         using holomorphic_on_imp_continuous_on[OF g_holo] 
-        by (auto simp add:continuous_on_def `r>0`) 
-      moreover have "at z within ball z r \<noteq> bot" using `r>0` 
+        by (auto simp add:continuous_on_def \<open>r>0\<close>) 
+      moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> 
         by (auto simp add:trivial_limit_within islimpt_ball)
       ultimately have "g z=0" by (auto intro: tendsto_unique)
-      thus False using asm `r>0` by auto
+      thus False using asm \<open>r>0\<close> by auto
     qed
   ultimately show "n=m" by fastforce
 qed
@@ -2220,18 +2220,18 @@
           g:"g holomorphic_on ball z r"
           "\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w" 
           "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
-    using holomorphic_factor_zero_nonconstant[OF holo `open s` `connected s` `z\<in>s` `f z=0`]
+    using holomorphic_factor_zero_nonconstant[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
     by (metis assms(3) assms(5) assms(6))
   def r'\<equiv>"r/2"
   have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
   hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'" 
       "(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
-    using g `ball z r \<subseteq> s` by auto
-  moreover have "r'>0" unfolding r'_def using `0<r` by auto
+    using g \<open>ball z r \<subseteq> s\<close> by auto
+  moreover have "r'>0" unfolding r'_def using \<open>0<r\<close> by auto
   ultimately show "\<exists>n g r. 0 < n \<and> 0 < r  \<and> g holomorphic_on cball z r 
           \<and> (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
     apply (intro exI[of _ n] exI[of _ g] exI[of _ r'])
-    by (simp add:`0 < n`)
+    by (simp add:\<open>0 < n\<close>)
 next
   fix m n 
   def fac\<equiv>"\<lambda>n g r. \<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0"  
@@ -2242,7 +2242,7 @@
   obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2"  
     and "fac m h r2" using m_asm by auto
   def r\<equiv>"min r1 r2"
-  have "r>0" using `r1>0` `r2>0` unfolding r_def by auto
+  have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
   moreover have "\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0" 
     using \<open>fac m h r2\<close> \<open>fac n g r1\<close>   unfolding fac_def r_def
     by fastforce
@@ -2257,11 +2257,11 @@
 proof
   fix p assume "p\<in>s"
   then obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> s" 
-    using open_contains_ball_eq[OF `open s`] by auto
+    using open_contains_ball_eq[OF \<open>open s\<close>] by auto
   obtain e2 where "0<e2" and "\<forall>x\<in>pts. x \<noteq> p \<longrightarrow> e2 \<le> dist p x" 
-    using finite_set_avoid[OF `finite pts`,of p] by auto
+    using finite_set_avoid[OF \<open>finite pts\<close>,of p] by auto
   hence "\<forall>w\<in>ball p (min e1 e2). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" using e1_b by auto
-  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` `e1>0` 
+  thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using \<open>e2>0\<close> \<open>e1>0\<close> 
     apply (rule_tac x="min e1 e2" in exI)
     by auto
 qed
@@ -2275,33 +2275,33 @@
   then obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" 
     using finite_ball_avoid[OF assms] by auto
   def e2\<equiv>"e1/2"
-  have "e2>0" and "e2<e1" unfolding e2_def using `e1>0` by auto
+  have "e2>0" and "e2<e1" unfolding e2_def using \<open>e1>0\<close> by auto
   then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
-  then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` e1 by auto
+  then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using \<open>e2>0\<close> e1 by auto
 qed
 
 lemma get_integrable_path:
   assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts"
   obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b" 
     "path_image g \<subseteq> s-pts" "f contour_integrable_on g" using assms
-proof (induct arbitrary:s thesis a rule:finite_induct[OF `finite pts`]) print_cases
+proof (induct arbitrary:s thesis a rule:finite_induct[OF \<open>finite pts\<close>]) print_cases
   case 1
   obtain g where "valid_path g" "path_image g \<subseteq> s" "pathstart g = a" "pathfinish g = b"
-    using connected_open_polynomial_connected[OF `open s`,of a b ] `connected (s - {})`
+    using connected_open_polynomial_connected[OF \<open>open s\<close>,of a b ] \<open>connected (s - {})\<close>
       valid_path_polynomial_function "1.prems"(6) "1.prems"(7) by auto
   moreover have "f contour_integrable_on g" 
-    using contour_integrable_holomorphic_simple[OF _ `open s` `valid_path g` `path_image g \<subseteq> s`,of f]
-      `f holomorphic_on s - {}`
+    using contour_integrable_holomorphic_simple[OF _ \<open>open s\<close> \<open>valid_path g\<close> \<open>path_image g \<subseteq> s\<close>,of f]
+      \<open>f holomorphic_on s - {}\<close>
     by auto
   ultimately show ?case using "1"(1)[of g] by auto
 next
   case idt:(2 p pts) 
   obtain e where "e>0" and e:"\<forall>w\<in>ball a e. w \<in> s \<and> (w \<noteq> a \<longrightarrow> w \<notin> insert p pts)"
-    using finite_ball_avoid[OF `open s` `finite (insert p pts)`,rule_format,of a]  
-      `a \<in> s - insert p pts`
+    using finite_ball_avoid[OF \<open>open s\<close> \<open>finite (insert p pts)\<close>,rule_format,of a]  
+      \<open>a \<in> s - insert p pts\<close>
     by auto
   def a'\<equiv>"a+e/2"
-  have "a'\<in>s-{p} -pts"  using e[rule_format,of "a+e/2"] `e>0`  
+  have "a'\<in>s-{p} -pts"  using e[rule_format,of "a+e/2"] \<open>e>0\<close>  
     by (auto simp add:dist_complex_def a'_def)
   then obtain g' where g'[simp]:"valid_path g'" "pathstart g' = a'" "pathfinish g' = b" 
     "path_image g' \<subseteq> s - {p} - pts" "f contour_integrable_on g'"    
@@ -2312,7 +2312,7 @@
   moreover have "pathstart g = a" and  "pathfinish g = b" unfolding g_def by auto 
   moreover have "path_image g \<subseteq> s - insert p pts" unfolding g_def 
     proof (rule subset_path_image_join)
-      have "closed_segment a a' \<subseteq> ball a e" using `e>0` 
+      have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close> 
         by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
       then show "path_image (linepath a a') \<subseteq> s - insert p pts" using e idt(9)
         by auto
@@ -2321,7 +2321,7 @@
     qed
   moreover have "f contour_integrable_on g"  
     proof -
-      have "closed_segment a a' \<subseteq> ball a e" using `e>0` 
+      have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close> 
         by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
       then have "continuous_on (closed_segment a a') f" 
         using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)]
@@ -2331,7 +2331,7 @@
         using contour_integrable_continuous_linepath by auto
       then show ?thesis unfolding g_def
         apply (rule contour_integrable_joinI)
-        by (auto simp add: `e>0`)
+        by (auto simp add: \<open>e>0\<close>)
     qed
   ultimately show ?case using idt.prems(1)[of g] by auto
 qed
@@ -2343,32 +2343,32 @@
           "\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
   shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
     using assms
-proof (induct arbitrary:s g rule:finite_induct[OF `finite pts`]) 
+proof (induct arbitrary:s g rule:finite_induct[OF \<open>finite pts\<close>]) 
   case 1
   then show ?case by (simp add: Cauchy_theorem_global contour_integral_unique)
 next
   case (2 p pts) 
-  note fin[simp] = `finite (insert p pts)`
-    and connected = `connected (s - insert p pts)`
-    and valid[simp] = `valid_path g`
-    and g_loop[simp] = `pathfinish g = pathstart g`
-    and holo[simp]= `f holomorphic_on s - insert p pts`
-    and path_img = `path_image g \<subseteq> s - insert p pts`
-    and winding = `\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0`
-    and h = `\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))`
+  note fin[simp] = \<open>finite (insert p pts)\<close>
+    and connected = \<open>connected (s - insert p pts)\<close>
+    and valid[simp] = \<open>valid_path g\<close>
+    and g_loop[simp] = \<open>pathfinish g = pathstart g\<close>
+    and holo[simp]= \<open>f holomorphic_on s - insert p pts\<close>
+    and path_img = \<open>path_image g \<subseteq> s - insert p pts\<close>
+    and winding = \<open>\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0\<close>
+    and h = \<open>\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))\<close>
   have "h p>0" and "p\<in>s"
     and h_p: "\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> insert p pts)"
-    using h `insert p pts \<subseteq> s` by auto
+    using h \<open>insert p pts \<subseteq> s\<close> by auto
   obtain pg where pg[simp]: "valid_path pg" "pathstart pg = pathstart g" "pathfinish pg=p+h p" 
       "path_image pg \<subseteq> s-insert p pts" "f contour_integrable_on pg" 
     proof -
       have "p + h p\<in>cball p (h p)" using h[rule_format,of p] 
         by (simp add: \<open>p \<in> s\<close> dist_norm)
-      then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] `insert p pts \<subseteq> s` 
+      then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close> 
         by fastforce
       moreover have "pathstart g \<in> s - insert p pts " using path_img by auto
       ultimately show ?thesis
-        using get_integrable_path[OF `open s` connected fin holo,of "pathstart g" "p+h p"] that
+        using get_integrable_path[OF \<open>open s\<close> connected fin holo,of "pathstart g" "p+h p"] that
         by blast
     qed
   obtain n::int where "n=winding_number g p"
@@ -2394,7 +2394,7 @@
         and "pathstart (n_circ 0) = p + h p"
         and "pathfinish (n_circ 0) = p + h p"
         and "p \<notin> path_image (n_circ 0)"
-        unfolding n_circ_def p_circ_pt_def using `h p > 0`
+        unfolding n_circ_def p_circ_pt_def using \<open>h p > 0\<close>
         by (auto simp add: dist_norm)
       show "winding_number (n_circ 0) p'=0 \<and> p'\<notin>path_image (n_circ 0)" when "p'\<notin>s- pts" for p' 
         unfolding n_circ_def p_circ_pt_def
@@ -2409,7 +2409,7 @@
       case (Suc k)
       have n_Suc:"n_circ (Suc k) = p_circ +++ n_circ k" unfolding n_circ_def by auto
       have pcirc:"p \<notin> path_image p_circ" "valid_path p_circ" "pathfinish p_circ = pathstart (n_circ k)" 
-        using Suc(3) unfolding p_circ_def using `h p > 0` by (auto simp add: p_circ_def)
+        using Suc(3) unfolding p_circ_def using \<open>h p > 0\<close> by (auto simp add: p_circ_def)
       have pcirc_image:"path_image p_circ \<subseteq> s - insert p pts" 
         proof -
           have "path_image p_circ \<subseteq> cball p (h p)" using \<open>0 < h p\<close> p_circ_def by auto
@@ -2426,15 +2426,15 @@
         proof -
           have "path_image p_circ = sphere p (h p)" 
             unfolding p_circ_def using \<open>0 < h p\<close> by auto
-          then show ?thesis unfolding n_Suc  using Suc.hyps(5)  `h p>0`
+          then show ?thesis unfolding n_Suc  using Suc.hyps(5)  \<open>h p>0\<close>
             by (auto simp add:  path_image_join[OF pcirc(3)]  dist_norm)
         qed
-      then show "p \<notin> path_image (n_circ (Suc k))" using `h p>0` by auto
+      then show "p \<notin> path_image (n_circ (Suc k))" using \<open>h p>0\<close> by auto
       show "winding_number (n_circ (Suc k)) p = of_nat (Suc k)" 
         proof -
           have "winding_number p_circ p = 1" 
-            by (simp add: `h p > 0` p_circ_def winding_number_circlepath_centre)
-          moreover have "p \<notin> path_image (n_circ k)" using Suc(5) `h p>0` by auto
+            by (simp add: \<open>h p > 0\<close> p_circ_def winding_number_circlepath_centre)
+          moreover have "p \<notin> path_image (n_circ k)" using Suc(5) \<open>h p>0\<close> by auto
           then have "winding_number (p_circ +++ n_circ k) p 
               = winding_number p_circ p + winding_number (n_circ k) p"
             using  valid_path_imp_path Suc.hyps(1) Suc.hyps(2) pcirc 
@@ -2485,14 +2485,14 @@
         using n_circ unfolding cp_def by auto
     next
       have "sphere p (h p) \<subseteq>  s - insert p pts" 
-        using h[rule_format,of p] `insert p pts \<subseteq> s` by force
+        using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close> by force
       moreover  have "p + complex_of_real (h p) \<in> s - insert p pts" 
         using pg(3) pg(4) by (metis pathfinish_in_path_image subsetCE)
       ultimately show "path_image cp \<subseteq>  s - insert p pts" unfolding cp_def
         using n_circ(5)  by auto
     next
       show "winding_number cp p = - n" 
-        unfolding cp_def using winding_number_reversepath n_circ `h p>0` by auto
+        unfolding cp_def using winding_number_reversepath n_circ \<open>h p>0\<close> by auto
     next
       show "winding_number cp p'=0 \<and> p' \<notin> path_image cp" when "p'\<notin>s - pts" for p'
         unfolding cp_def
@@ -2509,11 +2509,11 @@
     qed
   def g'\<equiv>"g +++ pg +++ cp +++ (reversepath pg)"
   have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)"
-    proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ `finite pts` ]) 
+    proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ \<open>finite pts\<close> ]) 
       show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
-      show "open (s - {p})" using `open s` by auto
-      show " pts \<subseteq> s - {p}" using `insert p pts \<subseteq> s` ` p \<notin> pts`  by blast 
-      show "f holomorphic_on s - {p} - pts" using holo `p \<notin> pts` by (metis Diff_insert2)
+      show "open (s - {p})" using \<open>open s\<close> by auto
+      show " pts \<subseteq> s - {p}" using \<open>insert p pts \<subseteq> s\<close> \<open> p \<notin> pts\<close>  by blast 
+      show "f holomorphic_on s - {p} - pts" using holo \<open>p \<notin> pts\<close> by (metis Diff_insert2)
       show "valid_path g'" 
         unfolding g'_def cp_def using n_circ valid pg g_loop
         by (auto intro!:valid_path_join )
@@ -2536,7 +2536,7 @@
           have "winding_number (g +++ pg +++ cp +++ reversepath pg) z = winding_number g z 
               + winding_number (pg +++ cp +++ (reversepath pg)) z"
             proof (rule winding_number_join)
-              show "path g" using `valid_path g` by simp
+              show "path g" using \<open>valid_path g\<close> by simp
               show "z \<notin> path_image g" using z path_img by auto
               show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp by auto
             next
@@ -2568,7 +2568,7 @@
           finally have "winding_number g' z = winding_number g z + winding_number cp z" 
             unfolding g'_def .
           moreover have "winding_number g z + winding_number cp z = 0" 
-            using winding z `n=winding_number g p` by auto
+            using winding z \<open>n=winding_number g p\<close> by auto
           ultimately show "winding_number g' z = 0" unfolding g'_def by auto
         qed
       show "\<forall>pa\<in>s - {p}. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s - {p} \<and> (w \<noteq> pa \<longrightarrow> w \<notin> pts))"
@@ -2581,7 +2581,7 @@
         + contour_integral (pg +++ cp +++ reversepath pg) f"
         unfolding g'_def
         apply (subst Cauchy_Integral_Thm.contour_integral_join) 
-        by (auto simp add:open_Diff[OF `open s`,OF finite_imp_closed[OF fin]]
+        by (auto simp add:open_Diff[OF \<open>open s\<close>,OF finite_imp_closed[OF fin]]
           intro!: contour_integrable_holomorphic_simple[OF holo _ _ path_img]  
           contour_integrable_reversepath)
       also have "... = contour_integral g f + contour_integral pg f 
@@ -2596,7 +2596,7 @@
         using contour_integral_reversepath
         by (auto simp add:contour_integrable_reversepath)
       also have "... = contour_integral g f - winding_number g p * contour_integral p_circ f"
-        using `n=winding_number g p` by auto
+        using \<open>n=winding_number g p\<close> by auto
       finally show ?thesis .
     qed
   moreover have "winding_number g' p' = winding_number g p'" when "p'\<in>pts" for p' 
@@ -2631,7 +2631,7 @@
   ultimately show ?case unfolding p_circ_def 
     apply (subst (asm) setsum.cong[OF refl, 
         of pts _ "\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"])
-    by (auto simp add:setsum.insert[OF `finite pts` `p\<notin>pts`] algebra_simps)         
+    by (auto simp add:setsum.insert[OF \<open>finite pts\<close> \<open>p\<notin>pts\<close>] algebra_simps)         
 qed  
 
 
@@ -2652,7 +2652,7 @@
   have "pts=pts1 \<union> pts2" "pts1 \<inter> pts2 = {}" "pts2 \<inter> s={}" "pts1\<subseteq>s" 
     unfolding pts1_def pts2_def by auto
   have "contour_integral g f =  (\<Sum>p\<in>pts1. circ p)" unfolding circ_def
-    proof (rule Cauchy_theorem_aux[OF `open s` _ _ `pts1\<subseteq>s` _ `valid_path g` loop _ homo])
+    proof (rule Cauchy_theorem_aux[OF \<open>open s\<close> _ _ \<open>pts1\<subseteq>s\<close> _ \<open>valid_path g\<close> loop _ homo])
       show "connected (s - pts1)" by (metis Diff_Int2 Int_absorb assms(2) pts1_def)
       show "finite pts1" using \<open>pts = pts1 \<union> pts2\<close> assms(3) by auto
       show "f holomorphic_on s - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def)
@@ -2663,14 +2663,14 @@
   moreover have "setsum circ pts2=0"
     proof -
       have "winding_number g p=0" when "p\<in>pts2" for p 
-        using  `pts2 \<inter> s={}` that homo[rule_format,of p] by auto
+        using  \<open>pts2 \<inter> s={}\<close> that homo[rule_format,of p] by auto
       thus ?thesis unfolding circ_def
         apply (intro setsum.neutral)
         by auto
     qed
   moreover have "?R=setsum circ pts1 + setsum circ pts2"
     unfolding circ_def 
-    using setsum.union_disjoint[OF _ _ `pts1 \<inter> pts2 = {}`] `finite pts` `pts=pts1 \<union> pts2`
+    using setsum.union_disjoint[OF _ _ \<open>pts1 \<inter> pts2 = {}\<close>] \<open>finite pts\<close> \<open>pts=pts1 \<union> pts2\<close>
     by blast
   ultimately show ?thesis
     apply (fold circ_def)
@@ -2717,8 +2717,8 @@
   have "(\<exists>!n. n>0 \<and> (\<exists> h r. P h r n))"
     proof -
       have "\<exists>!n. \<exists>h r. n>0 \<and> P h r n"
-        using holomorphic_factor_zero_Ex1[OF `open s` `connected s` `z\<in>s` holo `f z=0` 
-          `\<exists>w\<in>s. f w\<noteq>0`] unfolding P_def
+        using holomorphic_factor_zero_Ex1[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close> 
+          \<open>\<exists>w\<in>s. f w\<noteq>0\<close>] unfolding P_def
         apply (subst mult.commute)
         by auto
       thus ?thesis by auto
@@ -2738,10 +2738,10 @@
   obtain r2 where "r2>0" "cball z r2 \<subseteq> s" 
     using assms(3) assms(5) open_contains_cball_eq by blast
   def r3\<equiv>"min r1 r2"
-  have "P h r3 n" using `P h r1 n` `r2>0` unfolding P_def r3_def
+  have "P h r3 n" using \<open>P h r1 n\<close> \<open>r2>0\<close> unfolding P_def r3_def
     by auto
-  moreover have "cball z r3 \<subseteq> s" using `cball z r2 \<subseteq> s` unfolding r3_def by auto
-  ultimately show ?thesis using `n>0` unfolding P_def by auto
+  moreover have "cball z r3 \<subseteq> s" using \<open>cball z r2 \<subseteq> s\<close> unfolding r3_def by auto
+  ultimately show ?thesis using \<open>n>0\<close> unfolding P_def by auto
 qed    
 
 lemma porder_exist:  
@@ -2756,8 +2756,8 @@
   def zo\<equiv>"zorder (inverse \<circ> f) z" and zp\<equiv>"zer_poly (inverse \<circ> f) z"
   obtain r where "0 < zo" "0 < r" "cball z r \<subseteq> s" and zp_holo: "zp holomorphic_on cball z r" and
       zp_fac: "\<forall>w\<in>cball z r. (inverse \<circ> f) w = zp w * (w - z) ^ zo \<and> zp w \<noteq> 0"
-    using zorder_exist[OF `open s` `connected s` `z\<in>s` holo,folded zo_def zp_def] 
-      `f z=0` `\<exists>w\<in>s. f w\<noteq>0`
+    using zorder_exist[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo,folded zo_def zp_def] 
+      \<open>f z=0\<close> \<open>\<exists>w\<in>s. f w\<noteq>0\<close>
     by auto
   have n:"n=zo" and h:"h=inverse o zp" 
     unfolding n_def zo_def porder_def h_def zp_def pol_poly_def by simp_all
@@ -2767,8 +2767,8 @@
     using zp_fac unfolding h n comp_def
     by (metis divide_inverse_commute field_class.field_inverse_zero inverse_inverse_eq 
       inverse_mult_distrib mult.commute)
-  moreover have "0 < n" unfolding n using `zo>0` by simp
-  ultimately show ?thesis using `0 < r` `cball z r \<subseteq> s` by auto
+  moreover have "0 < n" unfolding n using \<open>zo>0\<close> by simp
+  ultimately show ?thesis using \<open>0 < r\<close> \<open>cball z r \<subseteq> s\<close> by auto
 qed
 
 lemma base_residue:  
@@ -2785,7 +2785,7 @@
       r_b:"cball z r \<subseteq> s" and
       h_holo:"h holomorphic_on cball z r" 
       and h:"(\<forall>w\<in>cball z r. f w = h w / (w - z) ^ n \<and> h w \<noteq> 0)"
-    using porder_exist[OF `open s` `connected s` `z\<in>s` holo `f z=0` non_c]
+    using porder_exist[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close> non_c]
     unfolding n_def h_def by auto
   def c\<equiv>"complex_of_real (2 * pi) * \<i>"
   have "residue f z =  (deriv ^^ (n - 1)) h z / fact (n-1)"
@@ -2795,15 +2795,15 @@
   then have "((\<lambda>u. h u / (u - z) ^ n) has_contour_integral c * residue f z)
           (circlepath z r)"
     using Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n -1"
-        ,unfolded Suc_diff_1[OF `n>0`],folded c_def] h_holo r_b
-    by (auto simp add:`r>0` holomorphic_on_imp_continuous_on holomorphic_on_subset)
+        ,unfolded Suc_diff_1[OF \<open>n>0\<close>],folded c_def] h_holo r_b
+    by (auto simp add:\<open>r>0\<close> holomorphic_on_imp_continuous_on holomorphic_on_subset)
   then have "(f has_contour_integral c * residue f z) (circlepath z r)"
     proof (elim has_contour_integral_eq)
       fix x assume "x \<in> path_image (circlepath z r)" 
       hence "x\<in>cball z r" using \<open>0 < r\<close> by auto
       then show "h x / (x - z) ^ n = f x" using h by auto
     qed
-  then show ?thesis using `r>0` `cball z r \<subseteq> s` unfolding c_def by auto
+  then show ?thesis using \<open>r>0\<close> \<open>cball z r \<subseteq> s\<close> unfolding c_def by auto
 qed
 
 theorem residue_theorem:
@@ -2822,26 +2822,26 @@
   def contour\<equiv>"\<lambda>p e. (f has_contour_integral c * residue f p) (circlepath p e)"
   def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
   have "poles \<subseteq> pts" and "finite pts"
-    using poles `finite {p. f p=0}` unfolding pts_def is_pole_def by auto
+    using poles \<open>finite {p. f p=0}\<close> unfolding pts_def is_pole_def by auto
   have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> contour p e)" 
       when "p\<in>s" for p 
     proof -
       obtain e1 where e:"e1>0" and e:"avoid p e1"
-        using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+        using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> unfolding avoid_def by auto
       have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> contour p e2"
         when "p\<in>poles" unfolding c_def contour_def
-        proof (rule base_residue[of "ball p e1" p f,simplified,OF `e1>0`])
+        proof (rule base_residue[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>])
           show "inverse \<circ> f holomorphic_on ball p e1" 
             proof -
               def f'\<equiv>"inverse o f"
               have "f holomorphic_on ball p e1 - {p}" 
-                using holo e `poles \<subseteq> pts` unfolding avoid_def
+                using holo e \<open>poles \<subseteq> pts\<close> unfolding avoid_def
                 apply (elim holomorphic_on_subset)
                 by auto
               then have f'_holo:"f' holomorphic_on ball p e1 - {p}" unfolding f'_def comp_def 
                 apply (elim holomorphic_on_inverse)
                 using e pts_def  ball_subset_cball unfolding avoid_def by blast
-              moreover have "isCont f' p" using `p\<in>poles` poles unfolding f'_def is_pole_def by auto
+              moreover have "isCont f' p" using \<open>p\<in>poles\<close> poles unfolding f'_def is_pole_def by auto
               ultimately show "f' holomorphic_on ball p e1"
                 apply (elim no_isolated_singularity[rotated])
                 apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
@@ -2849,10 +2849,10 @@
                   holomorphic_on_imp_differentiable_at by fastforce
             qed
         next
-          show "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+          show "f p = 0" using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
         next
           def p'\<equiv>"p+e1/2"
-          have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+          have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
           then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
             apply (rule_tac x=p' in bexI)
             by (auto simp add:pts_def)
@@ -2861,7 +2861,7 @@
       def e3\<equiv>"if p\<in>poles then e2 else e1"
       have "avoid p e3" 
         using e2 e that  avoid_def e3_def by auto
-      moreover have "e3>0" using `e1>0` e2 unfolding e3_def by auto        
+      moreover have "e3>0" using \<open>e1>0\<close> e2 unfolding e3_def by auto        
       moreover have " p\<in>poles \<longrightarrow> contour p e3" using e2 unfolding e3_def by auto 
       ultimately show ?thesis by auto
     qed  
@@ -2870,12 +2870,12 @@
   def cont\<equiv>"\<lambda>p. contour_integral (circlepath p (h p)) f"
   have "contour_integral \<gamma> f = (\<Sum>p\<in>poles. winding_number \<gamma> p * cont p)"
     unfolding cont_def
-    proof (rule Cauchy_theorem_singularities[OF `open s` `connected (s-poles)` _ holo `valid_path \<gamma>` 
-        loop `path_image \<gamma> \<subseteq> s-poles` homo])
-      show "finite poles" using `poles \<subseteq> pts` and `finite pts` by (simp add: finite_subset)
+    proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> \<open>connected (s-poles)\<close> _ holo \<open>valid_path \<gamma>\<close> 
+        loop \<open>path_image \<gamma> \<subseteq> s-poles\<close> homo])
+      show "finite poles" using \<open>poles \<subseteq> pts\<close> and \<open>finite pts\<close> by (simp add: finite_subset)
     next
       show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> poles))"
-        using   `poles \<subseteq> pts` h unfolding avoid_def by blast
+        using   \<open>poles \<subseteq> pts\<close> h unfolding avoid_def by blast
     qed
   also have "... = (\<Sum>p\<in>poles. c * (winding_number \<gamma> p * residue f p))" 
     proof (rule setsum.cong[of poles poles,simplified])
@@ -2886,7 +2886,7 @@
           then have "cont p=c*residue f p"
             unfolding cont_def
             apply (intro contour_integral_unique)
-            using h[unfolded contour_def] `p \<in> poles` by blast
+            using h[unfolded contour_def] \<open>p \<in> poles\<close> by blast
           then show ?thesis by auto
         next
           assume "p\<notin>s"
@@ -2925,12 +2925,12 @@
   def cont_zero\<equiv>"\<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)"
   def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
   have "poles \<subseteq> pts" and "zeros \<subseteq> pts" and "finite zeros" and "pts=zeros \<union> poles"
-    using poles `finite pts` unfolding pts_def zeros_def is_pole_def by auto
+    using poles \<open>finite pts\<close> unfolding pts_def zeros_def is_pole_def by auto
   have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> cont_pole ff p e) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p e)" 
       when "p\<in>s" for p 
     proof -
       obtain e1 where e:"e1>0" and e:"avoid p e1"
-        using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+        using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> unfolding avoid_def by auto
       have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
         when "p\<in>poles" 
         proof - 
@@ -2941,7 +2941,7 @@
           have "inverse \<circ> f holomorphic_on ball p e1" 
             proof -
               have "f holomorphic_on ball p e1 - {p}" 
-                using f_holo e `poles \<subseteq> pts` unfolding avoid_def
+                using f_holo e \<open>poles \<subseteq> pts\<close> unfolding avoid_def
                 apply (elim holomorphic_on_subset)
                 by auto
               then have inv_holo:"(inverse o f) holomorphic_on ball p e1 - {p}" 
@@ -2949,7 +2949,7 @@
                 apply (elim holomorphic_on_inverse)
                 using e pts_def  ball_subset_cball unfolding avoid_def by blast
               moreover have "isCont (inverse o f) p" 
-                using `p\<in>poles` poles unfolding is_pole_def by auto
+                using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
               ultimately show "(inverse o f) holomorphic_on ball p e1"
                 apply (elim no_isolated_singularity[rotated])
                 apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
@@ -2957,11 +2957,11 @@
                   holomorphic_on_imp_differentiable_at unfolding comp_def
                   by fastforce
             qed
-          moreover have "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+          moreover have "f p = 0" using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
           moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" 
             proof -
               def p'\<equiv>"p+e1/2"
-              have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+              have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
               then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
                 apply (rule_tac x=p' in bexI)
                 by (auto simp add:pts_def)
@@ -2971,50 +2971,50 @@
               "cball p r \<subseteq> ball p e1" and
               pp_holo:"pp holomorphic_on cball p r" and
               pp_po:"(\<forall>w\<in>cball p r. f w = pp w / (w - p) ^ po \<and> pp w \<noteq> 0)"
-            using porder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding po_def pp_def
+            using porder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] unfolding po_def pp_def
             by auto    
           def e2\<equiv>"r/2"
-          have "e2>0" using `r>0` unfolding e2_def by auto
+          have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
           def anal\<equiv>"\<lambda>w. deriv pp w * h w / pp w" and prin\<equiv>"\<lambda>w. - of_nat po * h w / (w - p)"
           have "((\<lambda>w.  prin w + anal w) has_contour_integral - c * po * h p) (circlepath p e2)"
             proof (rule  has_contour_integral_add[of _ _ _ _ 0,simplified])
               have "ball p r \<subseteq> s" 
                 using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
               then have "cball p e2 \<subseteq> s"
-                using `r>0` unfolding e2_def by auto  
+                using \<open>r>0\<close> unfolding e2_def by auto  
               then have "(\<lambda>w. - of_nat po * h w) holomorphic_on cball p e2" 
                 using h_holo
                 by (auto intro!: holomorphic_intros)
               then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)"
                 using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. - of_nat po * h w"]
-                  `e2>0`
+                  \<open>e2>0\<close>
                 unfolding prin_def
                 by (auto simp add: mult.assoc)
               have "anal holomorphic_on ball p r" unfolding anal_def 
-                using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+                using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close>
                 by (auto intro!: holomorphic_intros)
               then show "(anal has_contour_integral 0) (circlepath p e2)"
-                using e2_def `r>0`
+                using e2_def \<open>r>0\<close>
                 by (auto elim!: Cauchy_theorem_disc_simple)
             qed
           then have "cont_pole ff' p e2" unfolding cont_pole_def po_def
             proof (elim has_contour_integral_eq)
               fix w assume "w \<in> path_image (circlepath p e2)" 
-              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
               def wp\<equiv>"w-p"
               have "wp\<noteq>0" and "pp w \<noteq>0" 
-                unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto 
+                unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto 
               moreover have der_f':"deriv f' w = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" 
                 proof (rule DERIV_imp_deriv)
                   def der \<equiv> "- po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
-                  have po:"po = Suc (po - Suc 0) " using `po>0` by auto
+                  have po:"po = Suc (po - Suc 0) " using \<open>po>0\<close> by auto
                   have "(pp has_field_derivative (deriv pp w)) (at w)" 
-                    using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+                    using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
                           holomorphic_on_imp_differentiable_at[of _ "ball p r"] 
                           holomorphic_on_subset [OF pp_holo ball_subset_cball]
                     by (metis open_ball)
                   then show "(f' has_field_derivative  der) (at w)" 
-                    using `w\<noteq>p` `po>0` unfolding der_def f'_def
+                    using \<open>w\<noteq>p\<close> \<open>po>0\<close> unfolding der_def f'_def
                     apply (auto intro!: derivative_eq_intros simp add:field_simps)
                     apply (subst (4) po)
                     apply (subst power_Suc)
@@ -3030,7 +3030,7 @@
           then have "cont_pole ff p e2" unfolding cont_pole_def   
             proof (elim has_contour_integral_eq)
               fix w assume "w \<in> path_image (circlepath p e2)"
-              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
               have "deriv f' w =  deriv f w" 
               proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
                 show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
@@ -3038,14 +3038,14 @@
               next                
                 have "ball p e1 - {p} \<subseteq> s - poles" 
                   using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
-                then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+                then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
                   using ball_subset_cball by blast
                 then show "f holomorphic_on ball p r - {p}" using f_holo
                   by auto
               next
                 show "open (ball p r - {p})" by auto
               next
-                show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+                show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto
               next
                 fix x assume "x \<in> ball p r - {p}"
                 then show "f' x = f x" 
@@ -3058,7 +3058,7 @@
             qed
           moreover have "cball p e2 \<subseteq> ball p e1" 
             using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
-          ultimately show ?thesis using `e2>0` by auto
+          ultimately show ?thesis using \<open>e2>0\<close> by auto
         qed
       then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
         by auto
@@ -3075,12 +3075,12 @@
                 using \<open>poles \<subseteq> pts\<close> avoid_def ball_subset_cball e that zeros_def by fastforce
               thus ?thesis using f_holo by auto
             qed
-          moreover have "f p = 0" using `p\<in>zeros` 
+          moreover have "f p = 0" using \<open>p\<in>zeros\<close> 
             using DiffD1 mem_Collect_eq pts_def zeros_def by blast
           moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" 
             proof -
               def p'\<equiv>"p+e1/2"
-              have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+              have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
               then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
                 apply (rule_tac x=p' in bexI)
                 by (auto simp add:pts_def)
@@ -3090,50 +3090,50 @@
               "cball p r \<subseteq> ball p e1" and
               pp_holo:"zp holomorphic_on cball p r" and
               pp_po:"(\<forall>w\<in>cball p r. f w = zp w * (w - p) ^ zo \<and> zp w \<noteq> 0)"
-            using zorder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding zo_def zp_def
+            using zorder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] unfolding zo_def zp_def
             by auto    
           def e2\<equiv>"r/2"
-          have "e2>0" using `r>0` unfolding e2_def by auto
+          have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
           def anal\<equiv>"\<lambda>w. deriv zp w * h w / zp w" and prin\<equiv>"\<lambda>w. of_nat zo * h w / (w - p)"
           have "((\<lambda>w.  prin w + anal w) has_contour_integral c * zo * h p) (circlepath p e2)"
             proof (rule  has_contour_integral_add[of _ _ _ _ 0,simplified])
               have "ball p r \<subseteq> s" 
                 using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
               then have "cball p e2 \<subseteq> s"
-                using `r>0` unfolding e2_def by auto  
+                using \<open>r>0\<close> unfolding e2_def by auto  
               then have "(\<lambda>w. of_nat zo * h w) holomorphic_on cball p e2" 
                 using h_holo
                 by (auto intro!: holomorphic_intros)
               then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)"
                 using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. of_nat zo * h w"]
-                  `e2>0`
+                  \<open>e2>0\<close>
                 unfolding prin_def
                 by (auto simp add: mult.assoc)
               have "anal holomorphic_on ball p r" unfolding anal_def 
-                using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+                using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close>
                 by (auto intro!: holomorphic_intros)
               then show "(anal has_contour_integral 0) (circlepath p e2)"
-                using e2_def `r>0`
+                using e2_def \<open>r>0\<close>
                 by (auto elim!: Cauchy_theorem_disc_simple)
             qed
           then have "cont_zero ff' p e2" unfolding cont_zero_def zo_def
             proof (elim has_contour_integral_eq)
               fix w assume "w \<in> path_image (circlepath p e2)" 
-              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
               def wp\<equiv>"w-p"
               have "wp\<noteq>0" and "zp w \<noteq>0" 
-                unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto 
+                unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto 
               moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" 
                 proof (rule DERIV_imp_deriv)
                   def der\<equiv>"zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
-                  have po:"zo = Suc (zo - Suc 0) " using `zo>0` by auto
+                  have po:"zo = Suc (zo - Suc 0) " using \<open>zo>0\<close> by auto
                   have "(zp has_field_derivative (deriv zp w)) (at w)" 
-                    using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+                    using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
                           holomorphic_on_imp_differentiable_at[of _ "ball p r"] 
                           holomorphic_on_subset [OF pp_holo ball_subset_cball]
                     by (metis open_ball)
                   then show "(f' has_field_derivative  der) (at w)" 
-                    using `w\<noteq>p` `zo>0` unfolding der_def f'_def
+                    using \<open>w\<noteq>p\<close> \<open>zo>0\<close> unfolding der_def f'_def
                     by (auto intro!: derivative_eq_intros simp add:field_simps)
                 qed
               ultimately show "prin w + anal w = ff' w"
@@ -3147,7 +3147,7 @@
           then have "cont_zero ff p e2" unfolding cont_zero_def   
             proof (elim has_contour_integral_eq)
               fix w assume "w \<in> path_image (circlepath p e2)"
-              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+              then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
               have "deriv f' w =  deriv f w" 
                 proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
                   show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
@@ -3155,14 +3155,14 @@
                 next                
                   have "ball p e1 - {p} \<subseteq> s - poles" 
                     using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
-                  then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+                  then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
                     using ball_subset_cball by blast
                   then show "f holomorphic_on ball p r - {p}" using f_holo
                     by auto
                 next
                   show "open (ball p r - {p})" by auto
                 next
-                  show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+                  show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto
                 next
                   fix x assume "x \<in> ball p r - {p}"
                   then show "f' x = f x" 
@@ -3175,13 +3175,13 @@
             qed
           moreover have "cball p e2 \<subseteq> ball p e1" 
             using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
-          ultimately show ?thesis using `e2>0` by auto
+          ultimately show ?thesis using \<open>e2>0\<close> by auto
         qed
       then obtain e3 where e3:"p\<in>zeros \<longrightarrow> e3>0 \<and> cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3"
         by auto          
       def e4\<equiv>"if p\<in>poles then e2 else if p\<in>zeros then e3 else e1"
-      have "e4>0" using e2 e3 `e1>0` unfolding e4_def by auto
-      moreover have "avoid p e4" using e2 e3 `e1>0` e unfolding e4_def avoid_def by auto
+      have "e4>0" using e2 e3 \<open>e1>0\<close> unfolding e4_def by auto
+      moreover have "avoid p e4" using e2 e3 \<open>e1>0\<close> e unfolding e4_def avoid_def by auto
       moreover have "p\<in>poles \<longrightarrow> cont_pole ff p e4" and "p\<in>zeros \<longrightarrow> cont_zero ff p e4" 
         by (auto simp add: e2 e3 e4_def pts_def zeros_def)
       ultimately show ?thesis by auto
@@ -3193,17 +3193,17 @@
   def w\<equiv>"\<lambda>p. winding_number g p"
   have "contour_integral g ff = (\<Sum>p\<in>pts. w p * cont p)"
     unfolding cont_def w_def
-    proof (rule Cauchy_theorem_singularities[OF `open s` connected finite _ `valid_path g` loop 
+    proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> connected finite _ \<open>valid_path g\<close> loop 
         path_img homo])
-      have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] `open s` by auto 
-      then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo `poles \<subseteq> pts` h_holo
+      have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto 
+      then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo \<open>poles \<subseteq> pts\<close> h_holo
         by (auto intro!: holomorphic_intros simp add:pts_def)
     next
       show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts))"
         using get_e using avoid_def by blast
     qed
   also have "... = (\<Sum>p\<in>zeros. w p * cont p) + (\<Sum>p\<in>poles. w p * cont p)"
-    using `finite pts` unfolding `pts=zeros \<union> poles`
+    using \<open>finite pts\<close> unfolding \<open>pts=zeros \<union> poles\<close>
     apply (subst setsum.union_disjoint)
     by (auto simp add:zeros_def)
   also have "... = c * ((\<Sum>p\<in>zeros. w p *  h p * zorder f p) - (\<Sum>p\<in>poles. w p *  h p * porder f p))"
@@ -3216,7 +3216,7 @@
               assume "p \<in> s"
               have "cont p = c * h p * (zorder f p)" unfolding cont_def
                 apply (rule contour_integral_unique)
-                using get_e `p\<in>s` `p\<in>zeros` unfolding cont_zero_def                
+                using get_e \<open>p\<in>s\<close> \<open>p\<in>zeros\<close> unfolding cont_zero_def                
                 by (metis mult.assoc mult.commute)
               thus ?thesis by auto
             next
@@ -3236,7 +3236,7 @@
               assume "p \<in> s"
               have "cont p = - c * h p * (porder f p)" unfolding cont_def
                 apply (rule contour_integral_unique)
-                using get_e `p\<in>s` `p\<in>poles` unfolding cont_pole_def               
+                using get_e \<open>p\<in>s\<close> \<open>p\<in>poles\<close> unfolding cont_pole_def               
                 by (metis mult.assoc mult.commute)
               thus ?thesis by auto
             next
@@ -3259,7 +3259,7 @@
 proof (rule differentiable_at_imp_differentiable_on)
   fix x assume "x\<in>s"
   obtain f' where "(f has_field_derivative f') (at x) "
-    using holomorphic_on_imp_differentiable_at[OF f_holo `open s` `x\<in>s`] 
+    using holomorphic_on_imp_differentiable_at[OF f_holo \<open>open s\<close> \<open>x\<in>s\<close>] 
     unfolding field_differentiable_def by auto
   then have " (f has_derivative op * f') (at x)"
     using has_field_derivative_imp_has_derivative[of f f' "at x"] by auto
@@ -3290,8 +3290,8 @@
     proof -
       have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z 
         proof -
-          have "cmod (f z) > cmod (g z)" using `z\<in>path_image \<gamma>` path_less by auto
-          moreover have "f z = - g z"  using `f z + g z =0` by (simp add: eq_neg_iff_add_eq_0)
+          have "cmod (f z) > cmod (g z)" using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
+          moreover have "f z = - g z"  using \<open>f z + g z =0\<close> by (simp add: eq_neg_iff_add_eq_0)
           then have "cmod (f z) = cmod (g z)" by auto
           ultimately show False by auto
         qed
@@ -3301,8 +3301,8 @@
     proof -
       have False when "z\<in>path_image \<gamma>" and "f z =0" for z 
         proof -
-          have "cmod (g z) < cmod (f z) " using `z\<in>path_image \<gamma>` path_less by auto
-          then have "cmod (g z) < 0" using `f z=0` by auto          
+          have "cmod (g z) < cmod (f z) " using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
+          then have "cmod (g z) < 0" using \<open>f z=0\<close> by auto          
           then show False by auto
         qed
       then show ?thesis unfolding zeros_f_def using path_img by auto 
@@ -3312,7 +3312,7 @@
   def h\<equiv>"\<lambda>p. g p / f p + 1" 
   obtain spikes
     where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x"
-    using `valid_path \<gamma>`
+    using \<open>valid_path \<gamma>\<close>
     by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
   have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" 
     proof -
@@ -3334,12 +3334,12 @@
             by auto
         qed
       have valid_h:"valid_path (h \<circ> \<gamma>)"
-        proof (rule valid_path_compose_holomorphic[OF `valid_path \<gamma>` _ _ path_f])
+        proof (rule valid_path_compose_holomorphic[OF \<open>valid_path \<gamma>\<close> _ _ path_f])
           show "h holomorphic_on s - zeros_f" 
             unfolding h_def using f_holo g_holo
             by (auto intro!: holomorphic_intros simp add:zeros_f_def)
         next
-          show "open (s - zeros_f)" using `finite zeros_f` `open s` finite_imp_closed
+          show "open (s - zeros_f)" using \<open>finite zeros_f\<close> \<open>open s\<close> finite_imp_closed
             by auto
         qed
       have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)" 
@@ -3362,7 +3362,7 @@
       moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)"
           when "x\<in>{0..1} - spikes" for x 
         proof (rule vector_derivative_chain_at_general)
-          show "\<gamma> differentiable at x" using that `valid_path \<gamma>` spikes by auto
+          show "\<gamma> differentiable at x" using that \<open>valid_path \<gamma>\<close> spikes by auto
         next
           def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
           def t\<equiv>"\<gamma> x"
@@ -3374,13 +3374,13 @@
             unfolding h_def der_def using g_holo f_holo
             apply (auto intro!: derivative_eq_intros)
             by (auto simp add: DERIV_deriv_iff_field_differentiable 
-              holomorphic_on_imp_differentiable_at[OF _ `open s`])
+              holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>])
           then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto
         qed
       then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>) 
           = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"  
         unfolding has_contour_integral
-        apply (intro has_integral_spike_eq[OF negligible_finite, OF `finite spikes`])
+        apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>])
         by auto
       ultimately show ?thesis by auto
     qed
@@ -3390,8 +3390,8 @@
       + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" 
     proof -
       have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>" 
-        proof (rule contour_integrable_holomorphic_simple[OF _ _ `valid_path \<gamma>` path_f])
-          show "open (s - zeros_f)" using finite_imp_closed[OF `finite zeros_f`] `open s` 
+        proof (rule contour_integrable_holomorphic_simple[OF _ _ \<open>valid_path \<gamma>\<close> path_f])
+          show "open (s - zeros_f)" using finite_imp_closed[OF \<open>finite zeros_f\<close>] \<open>open s\<close> 
             by auto
           then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f"
             using f_holo
@@ -3420,23 +3420,23 @@
               ultimately show False by auto
             qed
           have der_fg:"deriv fg p =  deriv f p + deriv g p" unfolding fg_def
-            using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _  `open s`] path_img that
+            using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _  \<open>open s\<close>] path_img that
             by (auto intro!: deriv_add)
           have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)"
             proof -
               def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"          
               have "p\<in>s" using path_img that by auto
               then have "(h has_field_derivative der p) (at p)"
-                unfolding h_def der_def using g_holo f_holo `f p\<noteq>0`
+                unfolding h_def der_def using g_holo f_holo \<open>f p\<noteq>0\<close>
                 apply (auto intro!: derivative_eq_intros)
                 by (auto simp add: DERIV_deriv_iff_field_differentiable 
-                    holomorphic_on_imp_differentiable_at[OF _ `open s`])
+                    holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>])
               then show ?thesis unfolding der_def using DERIV_imp_deriv by auto
             qed
           show ?thesis
             apply (simp only:der_fg der_h)   
-            apply (auto simp add:field_simps `h p\<noteq>0` `f p\<noteq>0` `fg p\<noteq>0`)
-            by (auto simp add:field_simps h_def `f p\<noteq>0` fg_def) 
+            apply (auto simp add:field_simps \<open>h p\<noteq>0\<close> \<open>f p\<noteq>0\<close> \<open>fg p\<noteq>0\<close>)
+            by (auto simp add:field_simps h_def \<open>f p\<noteq>0\<close> fg_def) 
         qed
       then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p) 
           = contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)"
@@ -3445,19 +3445,19 @@
     qed
   moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
     unfolding c_def zeros_fg_def w_def 
-    proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+    proof (rule argument_principle[OF \<open>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
       show "connected (s - {p. fg p = 0})" using connected_fg unfolding zeros_fg_def .
       show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
       show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
-      show " finite {p. fg p = 0}" using `finite zeros_fg` unfolding zeros_fg_def .
+      show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
     qed
   moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
     unfolding c_def zeros_f_def w_def 
-    proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+    proof (rule argument_principle[OF \<open>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
       show "connected (s - {p. f p = 0})" using connected_f unfolding zeros_f_def .
       show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
       show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
-      show "finite {p. f p = 0}" using `finite zeros_f` unfolding zeros_f_def .
+      show "finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
     qed  
   ultimately have "c * (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
     by auto
diff -r 609f97d79bc2 -r 388719339ada src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Apr 03 23:57:32 2016 +0200
@@ -2409,7 +2409,7 @@
   using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
 
 text\<open>The case analysis eliminates the condition @{term "f integrable_on s"} at the cost
-     of the type class constraint @{text"division_ring"}\<close>
+     of the type class constraint \<open>division_ring\<close>\<close>
 corollary integral_mult_left [simp]:
   fixes c:: "'a::{real_normed_algebra,division_ring}"
   shows "integral s (\<lambda>x. f x * c) = integral s f * c"
diff -r 609f97d79bc2 -r 388719339ada src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/General/file.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -141,7 +141,15 @@
     if (path.is_file) path else error("No such file: " + path)
 
 
-  /* find files */
+  /* directory content */
+
+  def read_dir(dir: Path): List[String] =
+  {
+    if (!dir.is_dir) error("Bad directory: " + dir.toString)
+    val files = dir.file.listFiles
+    if (files == null) Nil
+    else files.toList.map(_.getName)
+  }
 
   def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
   {
diff -r 609f97d79bc2 -r 388719339ada src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Sun Apr 03 23:57:32 2016 +0200
@@ -57,12 +57,12 @@
   val empty =
     make_data (true,
       (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
-      (Symtab.make ML_Name_Space.initial_val,
-       Symtab.make ML_Name_Space.initial_type,
-       Symtab.make ML_Name_Space.initial_fixity,
-       Symtab.make ML_Name_Space.initial_structure,
-       Symtab.make ML_Name_Space.initial_signature,
-       Symtab.make ML_Name_Space.initial_functor),
+      (Symtab.make ML_Name_Space.sml_val,
+       Symtab.make ML_Name_Space.sml_type,
+       Symtab.make ML_Name_Space.sml_fixity,
+       Symtab.make ML_Name_Space.sml_structure,
+       Symtab.make ML_Name_Space.sml_signature,
+       Symtab.make ML_Name_Space.sml_functor),
       Inttab.empty);
   fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
   fun merge (data : T * T) =
diff -r 609f97d79bc2 -r 388719339ada src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Sun Apr 03 23:57:32 2016 +0200
@@ -40,30 +40,35 @@
   type valueVal = Values.value;
   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-  val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
   val forget_val = PolyML.Compiler.forgetValue;
 
   type typeVal = TypeConstrs.typeConstr;
   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-  val initial_type = #allType global ();
   val forget_type = PolyML.Compiler.forgetType;
 
   type fixityVal = Infixes.fixity;
   fun displayFix (_: string, x) = Infixes.print x;
-  val initial_fixity = #allFix global ();
 
   type structureVal = Structures.structureVal;
   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-  val initial_structure =
-    List.filter (fn (a, _) => not (List.exists (fn b => a = b) critical_structures))
-      (#allStruct global ());
   val forget_structure = PolyML.Compiler.forgetStructure;
 
   type signatureVal = Signatures.signatureVal;
   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-  val initial_signature = #allSig global ();
 
   type functorVal = Functors.functorVal;
   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
-  val initial_functor = #allFunct global ();
+
+
+  (* Standard ML name space *)
+
+  val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+  val sml_type = #allType global ();
+  val sml_fixity = #allFix global ();
+  val sml_structure =
+    List.filter (fn (a, _) => a <> "PolyML" andalso a <> "ML_System" andalso
+      not (List.exists (fn b => a = b) critical_structures)) (#allStruct global ());
+  val sml_signature =
+    List.filter (fn (a, _) => a <> "ML_SYSTEM" andalso a <> "ML_NAME_SPACE") (#allSig global ());
+  val sml_functor = #allFunct global ();
 end;
diff -r 609f97d79bc2 -r 388719339ada src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sun Apr 03 23:57:32 2016 +0200
@@ -6,7 +6,6 @@
 
 signature ISABELLE_SYSTEM =
 sig
-  val isabelle_tool: string -> string -> int
   val mkdirs: Path.T -> unit
   val mkdir: Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
@@ -37,29 +36,12 @@
   in rc end;
 
 
-(* system commands *)
-
-fun isabelle_tool name args =
-  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
-      let
-        val path = Path.append (Path.explode dir) (Path.basic name);
-        val platform_path = File.platform_path path;
-      in
-        if can OS.FileSys.modTime platform_path andalso
-          not (OS.FileSys.isDir platform_path) andalso
-          OS.FileSys.access (platform_path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
-        then SOME path
-        else NONE
-      end handle OS.SysErr _ => NONE) of
-    SOME path => bash (File.bash_path path ^ " " ^ args)
-  | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
+(* directory operations *)
 
 fun system_command cmd =
-  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
-  else ();
+  if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
 
-
-(* directory operations *)
+fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
 
 fun mkdirs path =
   if File.is_dir path then ()
@@ -112,8 +94,6 @@
 
 (* tmp dirs *)
 
-fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
-
 fun with_tmp_dir name f =
   let
     val path = create_tmp_path name "";
@@ -121,4 +101,3 @@
   in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
 
 end;
-
diff -r 609f97d79bc2 -r 388719339ada src/Pure/System/isabelle_tool.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -0,0 +1,109 @@
+/*  Title:      Pure/System/isabelle_tool.scala
+    Author:     Makarius
+
+Isabelle system tools: external executables or internal Scala functions.
+*/
+
+package isabelle
+
+
+object Isabelle_Tool
+{
+  /* external tools */
+
+  private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
+
+  private def is_external(dir: Path, name: String): Boolean =
+  {
+    val file = (dir + Path.basic(name)).file
+    try {
+      file.isFile && file.canRead && file.canExecute &&
+        !name.endsWith("~") && !name.endsWith(".orig")
+    }
+    catch { case _: SecurityException => false }
+  }
+
+  private def list_external(): List[(String, String)] =
+  {
+    val Description = """.*\bDESCRIPTION: *(.*)""".r
+    for {
+      dir <- dirs() if dir.is_dir
+      name <- File.read_dir(dir) if is_external(dir, name)
+    } yield {
+      val source = File.read(dir + Path.basic(name))
+      val description =
+        split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
+      (name, description)
+    }
+  }
+
+  private def find_external(name: String): Option[List[String] => Unit] =
+    dirs.collectFirst({ case dir if is_external(dir, name) =>
+      (args: List[String]) =>
+        {
+          val tool = dir + Path.basic(name)
+          val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
+          sys.exit(result.print_stdout.rc)
+        }
+    })
+
+
+  /* internal tools */
+
+  private var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
+
+  private def list_internal(): List[(String, String)] =
+    synchronized {
+      for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
+    }
+
+  private def find_internal(name: String): Option[List[String] => Unit] =
+    synchronized { internal_tools.get(name).map(_._2) }
+
+  private def register(isabelle_tool: Isabelle_Tool): Unit =
+    synchronized {
+      internal_tools +=
+        (isabelle_tool.name ->
+          (isabelle_tool.description,
+            args => Command_Line.tool0 { isabelle_tool.body(args) }))
+    }
+
+  register(Build.isabelle_tool)
+  register(Build_Doc.isabelle_tool)
+  register(Check_Sources.isabelle_tool)
+  register(Doc.isabelle_tool)
+  register(ML_Process.isabelle_tool)
+  register(Options.isabelle_tool)
+  register(Update_Cartouches.isabelle_tool)
+  register(Update_Header.isabelle_tool)
+  register(Update_Then.isabelle_tool)
+  register(Update_Theorems.isabelle_tool)
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool0 {
+      args.toList match {
+        case Nil | List("-?") =>
+          val tool_descriptions =
+            (list_external() ::: list_internal()).sortBy(_._1).
+              map({ case (a, "") => a case (a, b) => a + " - " + b })
+          Getopts("""
+Usage: isabelle TOOL [ARGS ...]
+
+  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
+
+Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
+        case tool_name :: tool_args =>
+          find_external(tool_name) orElse find_internal(tool_name) match {
+            case Some(tool) => tool(tool_args)
+            case None => error("Unknown Isabelle tool: " + quote(tool_name))
+          }
+      }
+    }
+  }
+}
+
+sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
diff -r 609f97d79bc2 -r 388719339ada src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/System/options.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -140,17 +140,16 @@
   val encode: XML.Encode.T[Options] = (options => options.encode)
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("option", "print Isabelle system options", args =>
   {
-    Command_Line.tool0 {
-      var build_options = false
-      var get_option = ""
-      var list_options = false
-      var export_file = ""
+    var build_options = false
+    var get_option = ""
+    var list_options = false
+    var export_file = ""
 
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
 
   Options are:
@@ -162,34 +161,33 @@
   Report Isabelle system options, augmented by MORE_OPTIONS given as
   arguments NAME=VAL or NAME.
 """,
-        "b" -> (_ => build_options = true),
-        "g:" -> (arg => get_option = arg),
-        "l" -> (_ => list_options = true),
-        "x:" -> (arg => export_file = arg))
+      "b" -> (_ => build_options = true),
+      "g:" -> (arg => get_option = arg),
+      "l" -> (_ => list_options = true),
+      "x:" -> (arg => export_file = arg))
 
-      val more_options = getopts(args)
-      if (get_option == "" && !list_options && export_file == "") getopts.usage()
+    val more_options = getopts(args)
+    if (get_option == "" && !list_options && export_file == "") getopts.usage()
 
-      val options =
-      {
-        val options0 = Options.init()
-        val options1 =
-          if (build_options)
-            (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
-          else options0
-        (options1 /: more_options)(_ + _)
-      }
+    val options =
+    {
+      val options0 = Options.init()
+      val options1 =
+        if (build_options)
+          (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
+        else options0
+      (options1 /: more_options)(_ + _)
+    }
 
-      if (get_option != "")
-        Console.println(options.check_name(get_option).value)
+    if (get_option != "")
+      Console.println(options.check_name(get_option).value)
 
-      if (export_file != "")
-        File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+    if (export_file != "")
+      File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
 
-      if (get_option == "" && export_file == "")
-        Console.println(options.print)
-    }
-  }
+    if (get_option == "" && export_file == "")
+      Console.println(options.print)
+  })
 }
 
 
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Thy/present.ML	Sun Apr 03 23:57:32 2016 +0200
@@ -269,8 +269,8 @@
         val doc_dir = Path.append doc_prefix (Path.basic doc_name);
         val _ = Isabelle_System.mkdirs doc_dir;
         val _ =
-          Isabelle_System.isabelle_tool "latex"
-            ("-o sty " ^ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
+          Isabelle_System.bash ("isabelle latex -o sty " ^
+            File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
         val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
         val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
         val _ = write_tex_index tex_index doc_dir;
@@ -360,8 +360,8 @@
     val _ = Isabelle_System.mkdirs doc_path;
     val root_path = Path.append doc_path (Path.basic "root.tex");
     val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
-    val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.bash_path root_path);
-    val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.bash_path root_path);
+    val _ = Isabelle_System.bash ("isabelle latex -o sty " ^ File.bash_path root_path);
+    val _ = Isabelle_System.bash ("isabelle latex -o syms " ^ File.bash_path root_path);
 
     fun known name =
       let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
@@ -382,8 +382,6 @@
     val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
     val _ = Isabelle_System.mkdirs target_dir;
     val _ = Isabelle_System.copy_file result target;
-  in
-    Isabelle_System.isabelle_tool "display" (File.bash_path target ^ " &")
-  end);
+  in Isabelle_System.bash ("isabelle display " ^ File.bash_path target ^ " &") end);
 
 end;
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/build.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -685,43 +685,40 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   {
-    Command_Line.tool {
-      def show_settings(): String =
-        cat_lines(List(
-          "ISABELLE_BUILD_OPTIONS=" +
-            quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
-          "ISABELLE_BUILD_JAVA_OPTIONS=" +
-            quote(Isabelle_System.getenv("ISABELLE_BUILD_JAVA_OPTIONS")),
-          "",
-          "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
-          "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
-          "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
-          "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
+    def show_settings(): String =
+      cat_lines(List(
+        "ISABELLE_BUILD_OPTIONS=" +
+          quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
+        "",
+        "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
+        "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
+        "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
+        "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
 
-      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+    val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
-      var select_dirs: List[Path] = Nil
-      var requirements = false
-      var exclude_session_groups: List[String] = Nil
-      var all_sessions = false
-      var build_heap = false
-      var clean_build = false
-      var dirs: List[Path] = Nil
-      var session_groups: List[String] = Nil
-      var max_jobs = 1
-      var check_keywords: Set[String] = Set.empty
-      var list_files = false
-      var no_build = false
-      var options = (Options.init() /: build_options)(_ + _)
-      var system_mode = false
-      var verbose = false
-      var exclude_sessions: List[String] = Nil
+    var select_dirs: List[Path] = Nil
+    var requirements = false
+    var exclude_session_groups: List[String] = Nil
+    var all_sessions = false
+    var build_heap = false
+    var clean_build = false
+    var dirs: List[Path] = Nil
+    var session_groups: List[String] = Nil
+    var max_jobs = 1
+    var check_keywords: Set[String] = Set.empty
+    var list_files = false
+    var no_build = false
+    var options = (Options.init() /: build_options)(_ + _)
+    var system_mode = false
+    var verbose = false
+    var exclude_sessions: List[String] = Nil
 
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
@@ -745,58 +742,57 @@
   Build and manage Isabelle sessions, depending on implicit settings:
 
 """ + Library.prefix_lines("  ", show_settings()),
-        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
-        "R" -> (_ => requirements = true),
-        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
-        "a" -> (_ => all_sessions = true),
-        "b" -> (_ => build_heap = true),
-        "c" -> (_ => clean_build = true),
-        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-        "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
-        "k:" -> (arg => check_keywords = check_keywords + arg),
-        "l" -> (_ => list_files = true),
-        "n" -> (_ => no_build = true),
-        "o:" -> (arg => options = options + arg),
-        "s" -> (_ => system_mode = true),
-        "v" -> (_ => verbose = true),
-        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+      "R" -> (_ => requirements = true),
+      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+      "a" -> (_ => all_sessions = true),
+      "b" -> (_ => build_heap = true),
+      "c" -> (_ => clean_build = true),
+      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+      "k:" -> (arg => check_keywords = check_keywords + arg),
+      "l" -> (_ => list_files = true),
+      "n" -> (_ => no_build = true),
+      "o:" -> (arg => options = options + arg),
+      "s" -> (_ => system_mode = true),
+      "v" -> (_ => verbose = true),
+      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
-      val sessions = getopts(args)
+    val sessions = getopts(args)
 
-      val progress = new Console_Progress(verbose)
+    val progress = new Console_Progress(verbose)
 
-      if (verbose) {
-        progress.echo(
-          Library.trim_line(
-            Isabelle_System.bash(
-              """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
-        progress.echo(show_settings() + "\n")
-      }
+    if (verbose) {
+      progress.echo(
+        Library.trim_line(
+          Isabelle_System.bash(
+            """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
+      progress.echo(show_settings() + "\n")
+    }
 
-      val start_time = Time.now()
-      val results =
-        progress.interrupt_handler {
-          build(options, progress, requirements, all_sessions, build_heap, clean_build,
-            dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
-            check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
-        }
-      val elapsed_time = Time.now() - start_time
+    val start_time = Time.now()
+    val results =
+      progress.interrupt_handler {
+        build(options, progress, requirements, all_sessions, build_heap, clean_build,
+          dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
+          check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
+      }
+    val elapsed_time = Time.now() - start_time
 
-      if (verbose) {
-        progress.echo("\n" +
-          Library.trim_line(
-            Isabelle_System.bash("""echo -n "Finished at "; date""").out))
-      }
+    if (verbose) {
+      progress.echo("\n" +
+        Library.trim_line(
+          Isabelle_System.bash("""echo -n "Finished at "; date""").out))
+    }
 
-      val total_timing =
-        (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
-          copy(elapsed = elapsed_time)
-      progress.echo(total_timing.message_resources)
+    val total_timing =
+      (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+        copy(elapsed = elapsed_time)
+    progress.echo(total_timing.message_resources)
 
-      results.rc
-    }
-  }
+    sys.exit(results.rc)
+  })
 
 
   /* PIDE protocol */
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/build_doc.scala
--- a/src/Pure/Tools/build_doc.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/build_doc.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -67,17 +67,16 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
   {
-    Command_Line.tool {
-      var all_docs = false
-      var max_jobs = 1
-      var system_mode = false
+    var all_docs = false
+    var max_jobs = 1
+    var system_mode = false
 
-      val getopts =
-        Getopts("""
+    val getopts =
+      Getopts("""
 Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
 
   Options are:
@@ -88,19 +87,20 @@
   Build Isabelle documentation from documentation sessions with
   suitable document_variants entry.
 """,
-        "a" -> (_ => all_docs = true),
-        "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
-        "s" -> (_ => system_mode = true))
+      "a" -> (_ => all_docs = true),
+      "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+      "s" -> (_ => system_mode = true))
+
+    val docs = getopts(args)
 
-      val docs = getopts(args)
+    if (!all_docs && docs.isEmpty) getopts.usage()
 
-      if (!all_docs && docs.isEmpty) getopts.usage()
-
-      val options = Options.init()
-      val progress = new Console_Progress()
+    val options = Options.init()
+    val progress = new Console_Progress()
+    val rc =
       progress.interrupt_handler {
         build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
       }
-    }
-  }
+    sys.exit(rc)
+  })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/check_sources.scala
--- a/src/Pure/Tools/check_sources.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/check_sources.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -52,11 +52,11 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
-  {
-    Command_Line.tool0 {
+  val isabelle_tool =
+    Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
+    {
       val getopts = Getopts("""
 Usage: isabelle check_sources [ROOT_DIRS...]
 
@@ -67,6 +67,5 @@
       if (specs.isEmpty) getopts.usage()
 
       for (root <- specs) check_hg(Path.explode(root))
-    }
-  }
+    })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/doc.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -91,28 +91,26 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
   {
-    Command_Line.tool0 {
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle doc [DOC ...]
 
   View Isabelle documentation.
 """)
-      val docs = getopts(args)
+    val docs = getopts(args)
 
-      val entries = contents()
-      if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
-      else {
-        docs.foreach(doc =>
-          entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
-            case Some(path) => view(path)
-            case None => error("No Isabelle documentation entry: " + quote(doc))
-          }
-        )
-      }
+    val entries = contents()
+    if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
+    else {
+      docs.foreach(doc =>
+        entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
+          case Some(path) => view(path)
+          case None => error("No Isabelle documentation entry: " + quote(doc))
+        }
+      )
     }
-  }
+  })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -102,18 +102,17 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
   {
-    Command_Line.tool {
-      var dirs: List[Path] = Nil
-      var eval_args: List[String] = Nil
-      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
-      var modes: List[String] = Nil
-      var options = Options.init()
+    var dirs: List[Path] = Nil
+    var eval_args: List[String] = Nil
+    var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+    var modes: List[String] = Nil
+    var options = Options.init()
 
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle process [OPTIONS]
 
   Options are:
@@ -127,20 +126,19 @@
 
   Run the raw Isabelle ML process in batch mode.
 """,
-        "T:" -> (arg =>
-          eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
-        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
-        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
-        "l:" -> (arg => logic = arg),
-        "m:" -> (arg => modes = arg :: modes),
-        "o:" -> (arg => options = options + arg))
+      "T:" -> (arg =>
+        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
+      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
+      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+      "l:" -> (arg => logic = arg),
+      "m:" -> (arg => modes = arg :: modes),
+      "o:" -> (arg => options = options + arg))
 
-      val more_args = getopts(args)
-      if (args.isEmpty || !more_args.isEmpty) getopts.usage()
+    val more_args = getopts(args)
+    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
 
-      ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
-        result().print_stdout.rc
-    }
-  }
+    ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
+      result().print_stdout.rc
+  })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_cartouches.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -82,11 +82,11 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
-  {
-    Command_Line.tool0 {
+  val isabelle_tool =
+    Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
+    {
       var replace_comment = false
       var replace_text = false
 
@@ -112,6 +112,5 @@
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
       } update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
-    }
-  }
+    })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_header.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -23,14 +23,14 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
   private val headings =
     Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
 
-  def main(args: Array[String])
-  {
-    Command_Line.tool0 {
+  val isabelle_tool =
+    Isabelle_Tool("update_header", "replace obsolete theory header command", args =>
+    {
       var section = "section"
 
       val getopts = Getopts("""
@@ -57,6 +57,5 @@
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
       } update_header(section, Path.explode(File.standard_path(file)))
-    }
-  }
+    })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/update_then.scala
--- a/src/Pure/Tools/update_then.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_then.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -28,11 +28,11 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
-  {
-    Command_Line.tool0 {
+  val isabelle_tool =
+    Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'", args =>
+    {
       val getopts = Getopts("""
 Usage: isabelle update_then [FILES|DIRS...]
 
@@ -51,6 +51,5 @@
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
       } update_then(Path.explode(File.standard_path(file)))
-    }
-  }
+    })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/Tools/update_theorems.scala
--- a/src/Pure/Tools/update_theorems.scala	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_theorems.scala	Sun Apr 03 23:57:32 2016 +0200
@@ -29,12 +29,11 @@
   }
 
 
-  /* command line entry point */
+  /* Isabelle tool wrapper */
 
-  def main(args: Array[String])
+  val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
   {
-    Command_Line.tool0 {
-      val getopts = Getopts("""
+    val getopts = Getopts("""
 Usage: isabelle update_theorems [FILES|DIRS...]
 
   Recursively find .thy files and update toplevel theorem keywords:
@@ -47,13 +46,12 @@
   Old versions of files are preserved by appending "~~".
 """)
 
-      val specs = getopts(args)
-      if (specs.isEmpty) getopts.usage()
+    val specs = getopts(args)
+    if (specs.isEmpty) getopts.usage()
 
-      for {
-        spec <- specs
-        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-      } update_theorems(Path.explode(File.standard_path(file)))
-    }
-  }
+    for {
+      spec <- specs
+      file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+    } update_theorems(Path.explode(File.standard_path(file)))
+  })
 }
diff -r 609f97d79bc2 -r 388719339ada src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/build-jars	Sun Apr 03 23:57:32 2016 +0200
@@ -81,6 +81,7 @@
   System/isabelle_charset.scala
   System/isabelle_process.scala
   System/isabelle_system.scala
+  System/isabelle_tool.scala
   System/options.scala
   System/platform.scala
   System/posix_interrupt.scala