simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;

--- a/Admin/README.repos	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/README.repos	Sat Oct 04 17:40:56 2008 +0200
@@ -11,7 +11,7 @@
 To work directly on a working copy of the repository, do the following:
 
 Change directory to "$ISABELLE/Distribution/bin" and execute:
-   ./isatool install -p ~/bin
+   ./isabelle install -p ~/bin
 
 This will install Isabelle executables in ~/bin.  Then issue in
 directory "$ISABELLE/Distribution"
@@ -33,7 +33,7 @@
 job.
 
 Now you can build images by going to corresponding folders and issuing:
-   isatool make
+   isabelle make
 
 (for instance, in "$ISABELLE/HOL" in order to make HOL).  This
 will create the directory "~/isabelle" (if not already present).

--- a/Admin/build	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/build	Sat Oct 04 17:40:56 2008 +0200
@@ -17,12 +17,12 @@
 ISABELLE_DIR="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 
 if [ -d "$ISABELLE_DIR/Distribution" ]; then
-  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isatool"
+  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isabelle"
   ISABELLE_LIB="$ISABELLE_DIR/Distribution/lib"
   ISABELLE_SRC="$ISABELLE_DIR"
   ISABELLE_DOC_SRC="$ISABELLE_DIR/Doc"
 else
-  ISABELLE_TOOL="$ISABELLE_DIR/bin/isatool"
+  ISABELLE_TOOL="$ISABELLE_DIR/bin/isabelle"
   ISABELLE_LIB="$ISABELLE_DIR/lib"
   ISABELLE_SRC="$ISABELLE_DIR/src"
   ISABELLE_DOC_SRC="$ISABELLE_DIR/doc-src"

--- a/Admin/check_ml_headers	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/check_ml_headers	Sat Oct 04 17:40:56 2008 +0200
@@ -19,7 +19,7 @@
   REPORT_EMPTY=1
 fi
 
-ISABELLE_SRC="$(isatool getenv -b ISABELLE_HOME)/src/"
+ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
 
 for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
 do

--- a/Admin/isatest/isatest-annomaly	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/isatest/isatest-annomaly	Sat Oct 04 17:40:56 2008 +0200
@@ -42,7 +42,7 @@
 ## main
 
 ISABELLE_HOME="$DISTPREFIX/Isabelle"
-ISABELLE_TOOL="$ISABELLE_HOME/bin/isatool"
+ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 
 [ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
 

--- a/Admin/isatest/isatest-check	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/isatest/isatest-check	Sat Oct 04 17:40:56 2008 +0200
@@ -97,7 +97,7 @@
 # generate development snapshot page only for successful tests
 # (failures in experimental sessions ok)
 if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
-  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool getenv ISABELLE_IDENTIFIER` make)
+  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv ISABELLE_IDENTIFIER` make)
   echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
 fi
 

--- a/Admin/isatest/isatest-doc	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/isatest/isatest-doc	Sat Oct 04 17:40:56 2008 +0200
@@ -25,7 +25,7 @@
 SHORT=at-poly
 SETTINGS=~/settings/$SHORT
 
-ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isatool
+ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isabelle
     
 
 MAIL=$HOME/bin/pmail

--- a/Admin/isatest/isatest-makeall	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/isatest/isatest-makeall	Sat Oct 04 17:40:56 2008 +0200
@@ -3,7 +3,7 @@
 # $Id$
 # Author: Gerwin Klein, TU Muenchen
 #
-# DESCRIPTION: Run isatool makeall from specified distribution and settings.
+# DESCRIPTION: Run isabelle makeall from specified distribution and settings.
 
 ## global settings
 . ~/admin/isatest/isatest-settings
@@ -20,7 +20,7 @@
   echo
   echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]"
   echo
-  echo "  Runs isatool makeall for specified settings."
+  echo "  Runs isabelle makeall for specified settings."
   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
   echo
   echo "Examples:"
@@ -88,7 +88,7 @@
         ;;
 esac
 
-ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isatool"
+ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
 
 [ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
 

--- a/Admin/makebin	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/makebin	Sat Oct 04 17:40:56 2008 +0200
@@ -101,12 +101,12 @@
     etc/settings
 fi
 
-ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
+ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   echo "### WARNING!  Personal Isabelle settings present. " >&2
 
-COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
-PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
+COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
+PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
 
 if [ -n "$DRY_RUN" ]; then
   mkdir -p "heaps/$COMPILER/log"

--- a/Admin/update-keywords	Sat Oct 04 16:19:49 2008 +0200
+++ b/Admin/update-keywords	Sat Oct 04 17:40:56 2008 +0200
@@ -5,19 +5,19 @@
 #
 # DESCRIPTION: Update standard keyword files.
 
-ISABELLE_HOME="$(isatool getenv -b ISABELLE_HOME)"
-LOG="$(isatool getenv -b ISABELLE_OUTPUT)"/log
+ISABELLE_HOME="$(isabelle getenv -b ISABELLE_HOME)"
+LOG="$(isabelle getenv -b ISABELLE_OUTPUT)"/log
 
 
 ## Emacs ProofGeneral
 
 cd "$ISABELLE_HOME/etc"
 
-isatool keywords -t emacs \
+isabelle keywords -t emacs \
   "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
   "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
 
-isatool keywords -t emacs -k ZF \
+isabelle keywords -t emacs -k ZF \
   "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
 
 
@@ -25,6 +25,6 @@
 
 cd "$ISABELLE_HOME/lib/jedit"
 
-isatool keywords -t jedit \
+isabelle keywords -t jedit \
   "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" \
   "$LOG/HOL-Statespace.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"

--- a/INSTALL	Sat Oct 04 16:19:49 2008 +0200
+++ b/INSTALL	Sat Oct 04 17:40:56 2008 +0200
@@ -36,13 +36,13 @@
 The installation may be finished as follows:
 
   cd [ISABELLE_HOME]
-  ./bin/isatool install -p /usr/local/bin
+  ./bin/isabelle install -p /usr/local/bin
 
 The install utility creates global references to the present Isabelle
 installation, enabling users to invoke the Isabelle executables
-without explicit path names.  Incidently, this is the only place where
-a static reference to [ISABELLE_HOME] is created; thus isatool install
-has to be run again whenever the Isabelle distribution is moved later.
+without explicit path names.  This is the only place where a static
+reference to [ISABELLE_HOME] is created; thus isabelle install has to
+be run again whenever the Isabelle distribution is moved later.
 
 
 Compiling logics
@@ -69,18 +69,18 @@
 Running the Isabelle binaries
 -----------------------------
 
-Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
-directly from their location within the distribution directory
-[ISABELLE_HOME] like this:
+Users may invoke the main Isabelle binaries (isabelle and
+isabelle-process) directly from their location within the distribution
+directory [ISABELLE_HOME] like this:
 
-  [ISABELLE_HOME]/bin/isabelle HOL
+  [ISABELLE_HOME]/bin/isabelle-process HOL
 
 This starts an interactive Isabelle session within the current text
 terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
 PATH.  An alternative is to create global references to the Isabelle
 executables as follows:
 
-  [ISABELLE_HOME]/bin/isatool install -p ~/bin
+  [ISABELLE_HOME]/bin/isabelle install -p ~/bin
 
 Note that the site-wide Isabelle installation may already provide
 Isabelle executables in some global bin directory (such as

--- a/NEWS	Sat Oct 04 16:19:49 2008 +0200
+++ b/NEWS	Sat Oct 04 17:40:56 2008 +0200
@@ -6,6 +6,31 @@
 
 *** General ***
 
+* Simplified main Isabelle executables, with less surprises on
+case-insensitive file-systems (such as Mac OS).
+
+  - The main Isabelle tool wrapper is now called "isabelle" instead of
+    "isatool."
+
+  - The former "isabelle" alias for "isabelle-process" has been
+    removed (should rarely occur to regular users).
+
+  - The "Isabelle" alias for "isabelle-interface" has been removed.
+
+Within scripts and make files, the Isabelle environment variables
+ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,
+respectively.  (The latter are still available as legacy feature.)
+
+Also note that user interfaces are now better wrapped as regular
+Isabelle tools instead of using the special isabelle-interface wrapper
+(which can be confusing if the interface is uninstalled or changed
+otherwise).  See "isabelle tty" and "isabelle emacs" for contemporary
+examples.
+
+INCOMPATIBILITY, need to adapt derivative scripts.  Users may need to
+purge installed copies of Isabelle executables and re-run "isabelle
+install -p ...", or use symlinks.
+
 * The Isabelle System Manual (system) has been updated, with formally
 checked references as hyperlinks.
 

--- a/bin/isabelle	Sat Oct 04 16:19:49 2008 +0200
+++ b/bin/isabelle	Sat Oct 04 17:40:56 2008 +0200
@@ -3,23 +3,76 @@
 # $Id$
 # Author: Markus Wenzel, TU Muenchen
 #
-# Smart selection of isabelle-process versus isabelle-interface.
+# Isabelle tool wrapper.
 
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
-THIS=$(cd "$(dirname "$0")"; pwd -P)
-NAME="$(basename "$0")"
+
+## settings
+
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+
+
+## diagnostics
 
-case "$NAME" in
-  I*)
-    PRG=isabelle-interface
-    ;;
-  i*)
-    PRG=isabelle-process
-    ;;
-esac
+function usage()
+{
+  echo
+  echo "Usage: $PRG TOOL [ARGS ...]"
+  echo
+  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
+  echo "  for more specific help."
+  echo
+  echo "  Available tools are:"
+  (
+    ORIG_IFS="$IFS"
+    IFS=":"
+    for DIR in $ISABELLE_TOOLS
+    do
+      cd "$DIR"
+      for T in *
+      do
+        if [ -f "$T" -a -x "$T" ]; then
+          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
+          echo "    $T - $DESCRLINE"
+        fi
+      done
+    done
+    IFS="$ORIG_IFS"
+  )
+  exit 1
+}
 
-exec "$THIS/$PRG" "$@"
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## args
+
+[ "$#" -lt 1 -o "$1" = "-?" ] && usage
+
+TOOLNAME="$1"
+shift
+
+
+## main
+
+ORIG_IFS="$IFS"
+IFS=":"
+for DIR in $ISABELLE_TOOLS
+do
+  TOOL="$DIR/$TOOLNAME"
+  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
+done
+IFS="$ORIG_IFS"
+
+fail "Unknown Isabelle tool: $TOOLNAME"

--- a/bin/isatool	Sat Oct 04 16:19:49 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# Isabelle tool starter.
-
-if [ -L "$0" ]; then
-  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
-  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-
-## settings
-
-PRG="$(basename "$0")"
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-
-## diagnostics
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG TOOL [ARGS ...]"
-  echo
-  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
-  echo "  for more specific help."
-  echo
-  echo "  Available tools are:"
-  (
-    ORIG_IFS="$IFS"
-    IFS=":"
-    for DIR in $ISABELLE_TOOLS
-    do
-      cd "$DIR"
-      for T in *
-      do
-        if [ -f "$T" -a -x "$T" ]; then
-          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
-          echo "    $T - $DESCRLINE"
-        fi
-      done
-    done
-    IFS="$ORIG_IFS"
-  )
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## args
-
-[ "$#" -lt 1 -o "$1" = "-?" ] && usage
-
-TOOLNAME="$1"
-shift
-
-
-## main
-
-ORIG_IFS="$IFS"
-IFS=":"
-for DIR in $ISABELLE_TOOLS
-do
-  TOOL="$DIR/$TOOLNAME"
-  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
-done
-IFS="$ORIG_IFS"
-
-fail "Unknown Isabelle tool: $TOOLNAME"

--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Sat Oct 04 16:19:49 2008 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Sat Oct 04 17:40:56 2008 +0200
@@ -18,10 +18,10 @@
   easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
   tools.  First invoke
 \begin{ttbox}
-  isatool mkdir Foo
+  isabelle mkdir Foo
 \end{ttbox}
   to initialize a separate directory for session @{verbatim Foo} ---
-  it is safe to experiment, since @{verbatim "isatool mkdir"} never
+  it is safe to experiment, since @{verbatim "isabelle mkdir"} never
   overwrites existing files.  Ensure that @{verbatim "Foo/ROOT.ML"}
   holds ML commands to load all theories required for this session;
   furthermore @{verbatim "Foo/document/root.tex"} should include any
@@ -33,7 +33,7 @@
   one level up from the @{verbatim Foo} directory location.  Now
   invoke
 \begin{ttbox}
-  isatool make Foo
+  isabelle make Foo
 \end{ttbox}
   to run the @{verbatim Foo} session, with browser information and
   document preparation enabled.  Unless any errors are reported by

--- a/doc-src/IsarRef/Thy/Introduction.thy	Sat Oct 04 16:19:49 2008 +0200
+++ b/doc-src/IsarRef/Thy/Introduction.thy	Sat Oct 04 17:40:56 2008 +0200
@@ -82,7 +82,7 @@
   the Isar interaction loop, with some support for command line
   editing.  For example:
 \begin{ttbox}
-isatool tty\medskip
+isabelle tty\medskip
 {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
 theory Foo imports Main begin;
 definition foo :: nat where "foo == 1";

--- a/doc-src/Ref/introduction.tex	Sat Oct 04 16:19:49 2008 +0200
+++ b/doc-src/Ref/introduction.tex	Sat Oct 04 17:40:56 2008 +0200
@@ -41,7 +41,7 @@
   \rangle\)/bin} to your search path.\footnote{Depending on your installation,
   there may be stand-alone binaries located in some global directory such as
   \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle isabellehome
-    \rangle\)/bin/isabelle}, though!  See \texttt{isatool install} in
+    \rangle\)/bin/isabelle}, though!  See \texttt{isabelle install} in
   \emph{The Isabelle System Manual} of how to do this properly.}
 
 \medskip
@@ -86,10 +86,10 @@
 called \texttt{ROOT.ML} that contains appropriate commands to load all other
 files required.  Running \texttt{isabelle} with option \texttt{-u}
 automatically loads \texttt{ROOT.ML} on entering the session.  The
-\texttt{isatool usedir} utility provides some more options to manage Isabelle
+\texttt{isabelle usedir} utility provides some more options to manage Isabelle
 sessions, such as automatic generation of theory browsing information.
 
-\medskip More details about the \texttt{isabelle} and \texttt{isatool}
+\medskip More details about the \texttt{isabelle} and \texttt{isabelle}
 commands may be found in \emph{The Isabelle System Manual}.
 
 \medskip There are more comfortable user interfaces than the bare-bones \ML{}

--- a/doc-src/System/Thy/Basics.thy	Sat Oct 04 16:19:49 2008 +0200
+++ b/doc-src/System/Thy/Basics.thy	Sat Oct 04 17:40:56 2008 +0200
@@ -22,22 +22,21 @@
   variables to all Isabelle programs (including tools and user
   interfaces).
 
-  \item The \emph{raw Isabelle process} (@{executable_ref isabelle} or
-  @{executable_ref "isabelle-process"}) runs logic sessions either
-  interactively or in batch mode.  In particular, this view abstracts
-  over the invocation of the actual ML system to be used.  Regular
-  users rarely need to care about the low-level process.
+  \item The \emph{raw Isabelle process} (@{executable_ref
+  "isabelle-process"}) runs logic sessions either interactively or in
+  batch mode.  In particular, this view abstracts over the invocation
+  of the actual ML system to be used.  Regular users rarely need to
+  care about the low-level process.
 
-  \item The \emph{Isabelle tools wrapper} (@{executable_ref isatool})
+  \item The \emph{Isabelle tools wrapper} (@{executable_ref isabelle})
   provides a generic startup environment Isabelle related utilities,
   user interfaces etc.  Such tools automatically benefit from the
   settings mechanism.
 
   \item The \emph{Isabelle interface wrapper} (@{executable_ref
-  Isabelle} or @{executable_ref "isabelle-interface"}) provides some
-  abstraction over the actual user interface to be used.  The de-facto
-  standard interface for Isabelle is Proof~General
-  \cite{proofgeneral}.
+  "isabelle-interface"}) provides some abstraction over the actual
+  user interface to be used.  The de-facto standard interface for
+  Isabelle is Proof~General \cite{proofgeneral}.
 
   \end{enumerate}
 *}
@@ -128,7 +127,7 @@
 
   \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
   automatically to the absolute path names of the @{executable
-  "isabelle-process"} and @{executable isatool} executables,
+  "isabelle-process"} and @{executable isabelle} executables,
   respectively.
   
   \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
@@ -171,7 +170,7 @@
   \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
   ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   names of the @{executable "isabelle-process"} and @{executable
-  isatool} executables, respectively.  Thus other tools and scripts
+  isabelle} executables, respectively.  Thus other tools and scripts
   need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is
   on the current search path of the shell.
   
@@ -234,8 +233,8 @@
   document preparation (see also \secref{sec:tool-latex}).
   
   \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
-  directories that are scanned by @{executable isatool} for external
-  utility programs (see also \secref{sec:isatool}).
+  directories that are scanned by @{executable isabelle} for external
+  utility programs (see also \secref{sec:isabelle-tool}).
   
   \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
   directories with documentation files.
@@ -269,11 +268,10 @@
 section {* The raw Isabelle process *}
 
 text {*
-  The @{executable_def isabelle} (or @{executable_def
-  "isabelle-process"}) executable runs bare-bones Isabelle logic
-  sessions --- either interactively or in batch mode.  It provides an
-  abstraction over the underlying ML system, and over the actual heap
-  file locations.  Its usage is:
+  The @{executable_def "isabelle-process"} executable runs bare-bones
+  Isabelle logic sessions --- either interactively or in batch mode.
+  It provides an abstraction over the underlying ML system, and over
+  the actual heap file locations.  Its usage is:
 
 \begin{ttbox}
 Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
@@ -430,14 +428,14 @@
 *}
 
 
-section {* The Isabelle tools wrapper \label{sec:isatool} *}
+section {* The Isabelle tools wrapper \label{sec:isabelle-tool} *}
 
 text {*
   All Isabelle related tools and interfaces are called via a common
-  wrapper --- @{executable isatool}:
+  wrapper --- @{executable isabelle}:
 
 \begin{ttbox}
-Usage: isatool TOOL [ARGS ...]
+Usage: isabelle TOOL [ARGS ...]
 
   Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
   for more specific help.
@@ -451,7 +449,7 @@
   In principle, Isabelle tools are ordinary executable scripts that
   are run within the Isabelle settings environment, see
   \secref{sec:settings}.  The set of available tools is collected by
-  @{executable isatool} from the directories listed in the @{setting
+  @{executable isabelle} from the directories listed in the @{setting
   ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
   from the shell.  Neither should you add the tool directories to your
   shell's search path!
@@ -465,22 +463,22 @@
   installation like this:
 
 \begin{ttbox}
-  isatool doc
+  isabelle doc
 \end{ttbox}
 
   View a certain document as follows:
 \begin{ttbox}
-  isatool doc isar-ref
+  isabelle doc isar-ref
 \end{ttbox}
 
   Create an Isabelle session derived from HOL (see also
   \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
 \begin{ttbox}
-  isatool mkdir HOL Test && isatool make
+  isabelle mkdir HOL Test && isabelle make
 \end{ttbox}
-  Note that @{verbatim "isatool mkdir"} is usually only invoked once;
+  Note that @{verbatim "isabelle mkdir"} is usually only invoked once;
   existing sessions (including document output etc.) are then updated
-  by @{verbatim "isatool make"} alone.
+  by @{verbatim "isabelle make"} alone.
 *}
 
 

--- a/doc-src/System/Thy/Misc.thy	Sat Oct 04 16:19:49 2008 +0200
+++ b/doc-src/System/Thy/Misc.thy	Sat Oct 04 17:40:56 2008 +0200
@@ -144,7 +144,7 @@
   Get the ML system name and the location where the compiler binaries
   are supposed to reside as follows:
 \begin{ttbox}
-isatool getenv ML_SYSTEM ML_HOME
+isabelle getenv ML_SYSTEM ML_HOME
 {\out ML_SYSTEM=polyml}
 {\out ML_HOME=/usr/share/polyml/x86-linux}
 \end{ttbox}
@@ -152,7 +152,7 @@
   The next one peeks at the output directory for Isabelle logic
   images:
 \begin{ttbox}
-isatool getenv -b ISABELLE_OUTPUT
+isabelle getenv -b ISABELLE_OUTPUT
 {\out /home/me/isabelle/heaps/polyml_x86-linux}
 \end{ttbox}
   Here we have used the @{verbatim "-b"} option to suppress the
@@ -171,11 +171,11 @@
 section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
 
 text {*
-  By default, the Isabelle binaries (@{executable "isabelle-process"},
-  @{executable isatool} etc.) are just run from their location within
-  the distribution directory, probably indirectly by the shell through
-  its @{setting PATH}.  Other schemes of installation are supported by
-  the @{tool_def install} utility:
+  By default, the main Isabelle binaries (@{executable "isabelle"}
+  etc.)  are just run from their location within the distribution
+  directory, probably indirectly by the shell through its @{setting
+  PATH}.  Other schemes of installation are supported by the
+  @{tool_def install} utility:
 \begin{ttbox}
 Usage: install [OPTIONS]
 
@@ -192,7 +192,7 @@
   distribution directory as determined by @{setting ISABELLE_HOME}.
 
   The @{verbatim "-p"} option installs executable wrapper scripts for
-  @{executable "isabelle-process"}, @{executable isatool},
+  @{executable "isabelle-process"}, @{executable isabelle},
   @{executable Isabelle}, containing proper absolute references to the
   Isabelle distribution directory.  A typical @{verbatim DIR}
   specification would be some directory expected to be in the shell's
@@ -218,7 +218,7 @@
     -q           quiet mode
 \end{ttbox}
   You are encouraged to use this to create a derived logo for your
-  Isabelle project.  For example, @{verbatim isatool} @{tool
+  Isabelle project.  For example, @{verbatim isabelle} @{tool
   logo}~@{verbatim Bali} creates @{verbatim isabelle_bali.eps}.
 *}
 
@@ -267,7 +267,7 @@
 \begin{ttbox}
 Usage: makeall [ARGS ...]
 
-  Apply isatool make to all logics (passing ARGS).
+  Apply isabelle make to all logics (passing ARGS).
 \end{ttbox}
 
   The arguments @{verbatim ARGS} are just passed verbatim to each

--- a/doc-src/System/Thy/Presentation.thy	Sat Oct 04 16:19:49 2008 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Sat Oct 04 17:40:56 2008 +0200
@@ -28,24 +28,24 @@
   \begin{center}
   \begin{tabular}{lp{0.6\textwidth}}
 
-      @{verbatim isatool} @{tool_ref mkdir} & invoked once by the user
+      @{verbatim isabelle} @{tool_ref mkdir} & invoked once by the user
       to create the initial source setup (common @{verbatim
       IsaMakefile} plus a single session directory); \\
 
-      @{verbatim isatool} @{tool make} & invoked repeatedly by the
+      @{verbatim isabelle} @{tool make} & invoked repeatedly by the
       user to keep session output up-to-date (HTML, documents etc.); \\
 
-      @{verbatim isatool} @{tool usedir} & part of the standard
+      @{verbatim isabelle} @{tool usedir} & part of the standard
       @{verbatim IsaMakefile} entry of a session; \\
 
       @{executable "isabelle-process"} & run through @{verbatim
-      isatool} @{tool_ref usedir}; \\
+      isabelle} @{tool_ref usedir}; \\
 
-      @{verbatim isatool} @{tool_ref document} & run by the Isabelle
+      @{verbatim isabelle} @{tool_ref document} & run by the Isabelle
       process if document preparation is enabled; \\
 
-      @{verbatim isatool} @{tool_ref latex} & universal {\LaTeX} tool
-      wrapper invoked multiple times by @{verbatim isatool} @{tool_ref
+      @{verbatim isabelle} @{tool_ref latex} & universal {\LaTeX} tool
+      wrapper invoked multiple times by @{verbatim isabelle} @{tool_ref
       document}; also useful for manual experiments; \\
 
   \end{tabular}
@@ -82,7 +82,7 @@
   The easiest way to let Isabelle generate theory browsing information
   for existing sessions is to append ``@{verbatim "-i true"}'' to the
   @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
-  isatool} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
+  isabelle} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
   example, add something like this to your Isabelle settings file
 
 \begin{ttbox}
@@ -90,7 +90,7 @@
 \end{ttbox}
 
   and then change into the @{"file" "~~/src/FOL"} directory and run
-  @{verbatim isatool} @{tool make}, or even @{verbatim isatool} @{tool
+  @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
   make}~@{verbatim all}.  The presentation output will appear in
   @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
   @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
@@ -130,19 +130,19 @@
   ISABELLE_BROWSER_INFO} to your WWW server, having generated browser
   info like this:
 \begin{ttbox}
-isatool usedir -i true HOL Foo
+isabelle usedir -i true HOL Foo
 \end{ttbox}
 
   This assumes that directory @{verbatim Foo} contains some @{verbatim
   ROOT.ML} file to load all your theories, and HOL is your parent
-  logic image (@{verbatim isatool} @{tool_ref mkdir} assists in
+  logic image (@{verbatim isabelle} @{tool_ref mkdir} assists in
   setting up Isabelle session directories.  Theory browser information
   for HOL should have been generated already beforehand.
   Alternatively, one may specify an external link to an existing body
   of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like
   this:
 \begin{ttbox}
-isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
+isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
 \end{ttbox}
 
   \medskip For production use, the @{tool usedir} tool is usually
@@ -151,7 +151,7 @@
   provide easy setup of all this, with only minimal manual editing
   required.
 \begin{ttbox}
-isatool mkdir HOL Foo && isatool make
+isabelle mkdir HOL Foo && isabelle make
 \end{ttbox}
   See \secref{sec:tool-mkdir} for more information on preparing
   Isabelle session directories, including the setup for documents.
@@ -169,7 +169,7 @@
   hidden, thus enabling the user to collapse irrelevant portions of
   information.  The browser is written in Java, it can be used both as
   a stand-alone application and as an applet.  Note that the option
-  @{verbatim "-g"} of @{verbatim isatool} @{tool_ref usedir} creates
+  @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates
   graph presentations in batch mode for inclusion in session
   documents.
 *}
@@ -342,7 +342,7 @@
   directory with a minimal @{verbatim root.tex} that is sufficient to
   print all theories of the session (in the order of appearance); see
   \secref{sec:tool-document} for further information on Isabelle
-  document preparation.  The usage of @{verbatim isatool} @{tool
+  document preparation.  The usage of @{verbatim isabelle} @{tool
   mkdir} is:
 
 \begin{ttbox}
@@ -406,12 +406,12 @@
   default logic, with proper document generation is generated like
   this:
 \begin{ttbox}
-isatool mkdir Foo && isatool make
+isabelle mkdir Foo && isabelle make
 \end{ttbox}
 
   \noindent The theory sources should be put into the @{verbatim Foo}
   directory, and its @{verbatim ROOT.ML} should be edited to load all
-  required theories.  Invoking @{verbatim isatool} @{tool make} again
+  required theories.  Invoking @{verbatim isabelle} @{tool make} again
   would run the whole session, generating browser information and the
   document automatically.  The @{verbatim IsaMakefile} is typically
   tuned manually later, e.g.\ adding source dependencies, or changing
@@ -423,7 +423,7 @@
   meant to cover all of the sub-session directories at the same time
   (this is the deeper reasong why @{verbatim IsaMakefile} is not made
   part of the initial session directory created by @{verbatim
-  isatool} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
+  isabelle} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
   a full-blown example.
 *}
 
@@ -546,10 +546,10 @@
   relative to the session's main directory.  If the @{verbatim "-C"}
   option is true, this will include a copy of an existing @{verbatim
   document} directory as provided by the user.  For example,
-  @{verbatim isatool} @{tool usedir}~@{verbatim "-D generated HOL
+  @{verbatim isabelle} @{tool usedir}~@{verbatim "-D generated HOL
   Foo"} produces a complete set of document sources at @{verbatim
   "Foo/generated"}.  Subsequent invocation of @{verbatim
-  isatool} @{tool document}~@{verbatim "Foo/generated"} (see also
+  isabelle} @{tool document}~@{verbatim "Foo/generated"} (see also
   \secref{sec:tool-document}) will process the final result
   independently of an Isabelle job.  This decoupled mode of operation
   facilitates debugging of serious {\LaTeX} errors, for example.
@@ -697,7 +697,7 @@
   "~~/lib/texinputs/pdfsetup.sty"} as well.
 
   \medskip As a final step of document preparation within Isabelle,
-  @{verbatim isatool} @{tool document}~@{verbatim "-c"} is run on the
+  @{verbatim isabelle} @{tool document}~@{verbatim "-c"} is run on the
   resulting @{verbatim document} directory.  Thus the actual output
   document is built and installed in its proper place (as linked by
   the session's @{verbatim index.html} if option @{verbatim "-i"} of
@@ -748,7 +748,7 @@
 subsubsection {* Examples *}
 
 text {*
-  Invoking @{verbatim isatool} @{tool latex} by hand may be
+  Invoking @{verbatim isabelle} @{tool latex} by hand may be
   occasionally useful when debugging failed attempts of the automatic
   document preparation stage of batch-mode Isabelle.  The abortive
   process leaves the sources at a certain place within @{setting
@@ -757,7 +757,7 @@
   like this:
 \begin{ttbox}
   cd ~/isabelle/browser_info/HOL/Test/document
-  isatool latex -o pdf
+  isabelle latex -o pdf
 \end{ttbox}
 *}
 

--- a/doc-src/TutorialI/Documents/Documents.thy	Sat Oct 04 16:19:49 2008 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Sat Oct 04 17:40:56 2008 +0200
@@ -347,18 +347,18 @@
   (usually rooted at \verb,~/isabelle/browser_info,).
 
   \medskip The easiest way to manage Isabelle sessions is via
-  \texttt{isatool mkdir} (generates an initial session source setup)
-  and \texttt{isatool make} (run sessions controlled by
+  \texttt{isabelle mkdir} (generates an initial session source setup)
+  and \texttt{isabelle make} (run sessions controlled by
   \texttt{IsaMakefile}).  For example, a new session
   \texttt{MySession} derived from \texttt{HOL} may be produced as
   follows:
 
 \begin{verbatim}
-  isatool mkdir HOL MySession
-  isatool make
+  isabelle mkdir HOL MySession
+  isabelle make
 \end{verbatim}
 
-  The \texttt{isatool make} job also informs about the file-system
+  The \texttt{isabelle make} job also informs about the file-system
   location of the ultimate results.  The above dry run should be able
   to produce some \texttt{document.pdf} (with dummy title, empty table
   of contents etc.).  Any failure at this stage usually indicates
@@ -394,7 +394,7 @@
   several sessions may be managed by the same \texttt{IsaMakefile}.
   See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
   for further details, especially on
-  \texttt{isatool usedir} and \texttt{isatool make}.
+  \texttt{isabelle usedir} and \texttt{isabelle make}.
 
   \end{itemize}
 
@@ -417,7 +417,7 @@
   \texttt{MySession/document} directory as well.  In particular,
   adding a file named \texttt{root.bib} causes an automatic run of
   \texttt{bibtex} to process a bibliographic database; see also
-  \texttt{isatool document} \cite{isabelle-sys}.
+  \texttt{isabelle document} \cite{isabelle-sys}.
 
   \medskip Any failure of the document preparation phase in an
   Isabelle batch session leaves the generated sources in their target
@@ -753,7 +753,7 @@
   tagged region, in order to keep, drop, or fold the corresponding
   parts of the document.  See the \emph{Isabelle System Manual}
   \cite{isabelle-sys} for further details, especially on
-  \texttt{isatool usedir} and \texttt{isatool document}.
+  \texttt{isabelle usedir} and \texttt{isabelle document}.
 
   Ignored material is specified by delimiting the original formal
   source with special source comments

--- a/etc/settings	Sat Oct 04 16:19:49 2008 +0200
+++ b/etc/settings	Sat Oct 04 17:40:56 2008 +0200
@@ -82,7 +82,7 @@
 
 
 ###
-### Interactive sessions (cf. isatool tty)
+### Interactive sessions (cf. isabelle tty)
 ###
 
 ISABELLE_LINE_EDITOR=""
@@ -91,7 +91,7 @@
 
 
 ###
-### Batch sessions (cf. isatool usedir)
+### Batch sessions (cf. isabelle usedir)
 ###
 
 ISABELLE_USEDIR_OPTIONS="-p 1 -v true -V outline=/proof,/ML"
@@ -109,7 +109,7 @@
 
 
 ###
-### Document preparation (cf. isatool latex/document)
+### Document preparation (cf. isabelle latex/document)
 ###
 
 ISABELLE_LATEX="latex"

--- a/lib/Tools/install	Sat Oct 04 16:19:49 2008 +0200
+++ b/lib/Tools/install	Sat Oct 04 17:40:56 2008 +0200
@@ -74,7 +74,7 @@
 if [ -n "$BINDIR" ]; then
   mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
 
-  for NAME in isatool isabelle-process isabelle-interface
+  for NAME in isabelle isabelle-process isabelle-interface
   do
     BIN="$BINDIR/$NAME"
     DIST="$DISTDIR/bin/$NAME"
@@ -85,12 +85,4 @@
     echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
     chmod +x "$BIN"
   done
-  for NAME in Isabelle isabelle
-  do
-    BIN="$BINDIR/$NAME"
-    echo "installing $BIN"
-    rm -f "$BIN"
-    cp "$ISABELLE_HOME/bin/$NAME" "$BIN" || fail "Cannot write file: $BIN"
-    chmod +x "$BIN"
-  done
 fi

--- a/lib/Tools/makeall	Sat Oct 04 16:19:49 2008 +0200
+++ b/lib/Tools/makeall	Sat Oct 04 17:40:56 2008 +0200
@@ -19,7 +19,7 @@
   echo
   echo "Usage: $PRG [ARGS ...]"
   echo
-  echo "  Apply isatool make to all logics (passing ARGS)."
+  echo "  Apply isabelle make to all logics (passing ARGS)."
   echo
   exit 1
 }

--- a/lib/Tools/mkdir	Sat Oct 04 16:19:49 2008 +0200
+++ b/lib/Tools/mkdir	Sat Oct 04 17:40:56 2008 +0200
@@ -281,7 +281,7 @@
 
 Notes:
 
-  * 'isatool make' processes the session (including document preparation)
+  * 'isabelle make' processes the session (including document preparation)
 
   * $DIR/IsaMakefile contains compilation options and file dependencies
 

--- a/lib/logo/index.html	Sat Oct 04 16:19:49 2008 +0200
+++ b/lib/logo/index.html	Sat Oct 04 17:40:56 2008 +0200
@@ -22,7 +22,7 @@
 href="isabelle-small.xpm">small</a> and <a
 href="isabelle-tiny.xpm">tiny</a> Isabelle icons available.
 Furthermore, scalable (EPS) versions of the logo may be generated for
-any logic using the <tt>isatool logo</tt> utility distributed with
+any logic using the <tt>isabelle logo</tt> utility distributed with
 Isabelle.
 
 

--- a/lib/scripts/getsettings	Sat Oct 04 16:19:49 2008 +0200
+++ b/lib/scripts/getsettings	Sat Oct 04 17:40:56 2008 +0200
@@ -20,7 +20,7 @@
 
 #key executables
 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
-ISABELLE_TOOL="$ISABELLE_HOME/bin/isatool"
+ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 #legacy settings
 ISABELLE="$ISABELLE_PROCESS"
 ISATOOL="$ISABELLE_TOOL"

--- a/lib/texinputs/draft.tex	Sat Oct 04 16:19:49 2008 +0200
+++ b/lib/texinputs/draft.tex	Sat Oct 04 17:40:56 2008 +0200
@@ -7,7 +7,7 @@
 \documentclass[10pt,a4paper]{article}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
-%packages for unusual symbols according to 'isatool latex -o syms'
+%packages for unusual symbols according to 'isabelle latex -o syms'
 \usepackage[latin1]{inputenc}
 \usepackage{amssymb}
 \usepackage{textcomp}

--- a/src/HOL/Import/HOL/README	Sat Oct 04 16:19:49 2008 +0200
+++ b/src/HOL/Import/HOL/README	Sat Oct 04 17:40:56 2008 +0200
@@ -5,10 +5,10 @@
 
 All the files in this directory (except this README, HOL4.thy, and
 ROOT.ML) are automatically generated.  Edit the files in
-../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in
+../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" in
 ~~/src/HOL, if something needs to be changed.
 
-To build the logic in this directory, simply do a "isatool make
+To build the logic in this directory, simply do a "isabelle make
 HOL-Import-HOL" in ~~/src/HOL.
 
 Note that the quick_and_dirty flag is on as default for this
@@ -17,4 +17,4 @@
 unpack the HOL4 proof objects to somewhere on your harddisk, and set
 the variable PROOF_DIRS to the directory where the directory "hol4"
 is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
-do "isatool make HOL-Import-HOL" in ~~/src/HOL.
+do "isabelle make HOL-Import-HOL" in ~~/src/HOL.

--- a/src/HOL/Library/README.html	Sat Oct 04 16:19:49 2008 +0200
+++ b/src/HOL/Library/README.html	Sat Oct 04 17:40:56 2008 +0200
@@ -74,7 +74,7 @@
 
 <dd>Non-ASCII symbols should be used as appropriate, with some
 care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
-be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool
+be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isabelle
 unsymbolize</tt> to clean up the sources.
 
 <p>

--- a/src/HOL/Nominal/INSTALL	Sat Oct 04 16:19:49 2008 +0200
+++ b/src/HOL/Nominal/INSTALL	Sat Oct 04 17:40:56 2008 +0200
@@ -21,7 +21,7 @@
 
 After the build completes, install the files with the command
 
-   ./bin/isatool install -p /usr/local/bin
+   ./bin/isabelle install -p /usr/local/bin
 
 where /usr/local/bin needs to be replaced by an appropriate
 directory, if you are not root on the system. 

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 04 16:19:49 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 04 17:40:56 2008 +0200
@@ -747,7 +747,7 @@
     let
         val arg = #arg vs
     in
-        isarcmd ("print_" ^ arg)   (* FIXME: isatool doc?.  Return URLs, maybe? *)
+        isarcmd ("print_" ^ arg)   (* FIXME: isabelle doc?.  Return URLs, maybe? *)
     end
 
 (*** Theory ***)

--- a/src/Pure/README	Sat Oct 04 16:19:49 2008 +0200
+++ b/src/Pure/README	Sat Oct 04 17:40:56 2008 +0200
@@ -6,16 +6,16 @@
 is the basis for all object-logics.  The Isabelle/Pure image may be
 compiled in batch mode like this:
 
-  isatool make Pure
+  isabelle make Pure
 
 Developers may want to produce a RAW image that merely consists of the
 ML compiler with the compatibility setup of ML-Systems/ preloaded:
 
-  isatool make RAW
+  isabelle make RAW
 
 Now the Pure session may be compiled interactively as follows:
 
-  isabelle -u RAW
+  isabelle-process -u RAW
 
 See ROOT.ML for further information.