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

     2.1 --- a/Admin/build	Sat Oct 04 16:19:49 2008 +0200
     2.2 +++ b/Admin/build	Sat Oct 04 17:40:56 2008 +0200
     2.3 @@ -17,12 +17,12 @@
     2.4  ISABELLE_DIR="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
     2.5  
     2.6  if [ -d "$ISABELLE_DIR/Distribution" ]; then
     2.7 -  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isatool"
     2.8 +  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isabelle"
     2.9    ISABELLE_LIB="$ISABELLE_DIR/Distribution/lib"
    2.10    ISABELLE_SRC="$ISABELLE_DIR"
    2.11    ISABELLE_DOC_SRC="$ISABELLE_DIR/Doc"
    2.12  else
    2.13 -  ISABELLE_TOOL="$ISABELLE_DIR/bin/isatool"
    2.14 +  ISABELLE_TOOL="$ISABELLE_DIR/bin/isabelle"
    2.15    ISABELLE_LIB="$ISABELLE_DIR/lib"
    2.16    ISABELLE_SRC="$ISABELLE_DIR/src"
    2.17    ISABELLE_DOC_SRC="$ISABELLE_DIR/doc-src"

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

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

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

     6.1 --- a/Admin/isatest/isatest-doc	Sat Oct 04 16:19:49 2008 +0200
     6.2 +++ b/Admin/isatest/isatest-doc	Sat Oct 04 17:40:56 2008 +0200
     6.3 @@ -25,7 +25,7 @@
     6.4  SHORT=at-poly
     6.5  SETTINGS=~/settings/$SHORT
     6.6  
     6.7 -ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isatool
     6.8 +ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isabelle
     6.9      
    6.10  
    6.11  MAIL=$HOME/bin/pmail

     7.1 --- a/Admin/isatest/isatest-makeall	Sat Oct 04 16:19:49 2008 +0200
     7.2 +++ b/Admin/isatest/isatest-makeall	Sat Oct 04 17:40:56 2008 +0200
     7.3 @@ -3,7 +3,7 @@
     7.4  # $Id$
     7.5  # Author: Gerwin Klein, TU Muenchen
     7.6  #
     7.7 -# DESCRIPTION: Run isatool makeall from specified distribution and settings.
     7.8 +# DESCRIPTION: Run isabelle makeall from specified distribution and settings.
     7.9  
    7.10  ## global settings
    7.11  . ~/admin/isatest/isatest-settings
    7.12 @@ -20,7 +20,7 @@
    7.13    echo
    7.14    echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]"
    7.15    echo
    7.16 -  echo "  Runs isatool makeall for specified settings."
    7.17 +  echo "  Runs isabelle makeall for specified settings."
    7.18    echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
    7.19    echo
    7.20    echo "Examples:"
    7.21 @@ -88,7 +88,7 @@
    7.22          ;;
    7.23  esac
    7.24  
    7.25 -ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isatool"
    7.26 +ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
    7.27  
    7.28  [ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
    7.29  

     8.1 --- a/Admin/makebin	Sat Oct 04 16:19:49 2008 +0200
     8.2 +++ b/Admin/makebin	Sat Oct 04 17:40:56 2008 +0200
     8.3 @@ -101,12 +101,12 @@
     8.4      etc/settings
     8.5  fi
     8.6  
     8.7 -ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
     8.8 +ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
     8.9  [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
    8.10    echo "### WARNING!  Personal Isabelle settings present. " >&2
    8.11  
    8.12 -COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
    8.13 -PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
    8.14 +COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
    8.15 +PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
    8.16  
    8.17  if [ -n "$DRY_RUN" ]; then
    8.18    mkdir -p "heaps/$COMPILER/log"

     9.1 --- a/Admin/update-keywords	Sat Oct 04 16:19:49 2008 +0200
     9.2 +++ b/Admin/update-keywords	Sat Oct 04 17:40:56 2008 +0200
     9.3 @@ -5,19 +5,19 @@
     9.4  #
     9.5  # DESCRIPTION: Update standard keyword files.
     9.6  
     9.7 -ISABELLE_HOME="$(isatool getenv -b ISABELLE_HOME)"
     9.8 -LOG="$(isatool getenv -b ISABELLE_OUTPUT)"/log
     9.9 +ISABELLE_HOME="$(isabelle getenv -b ISABELLE_HOME)"
    9.10 +LOG="$(isabelle getenv -b ISABELLE_OUTPUT)"/log
    9.11  
    9.12  
    9.13  ## Emacs ProofGeneral
    9.14  
    9.15  cd "$ISABELLE_HOME/etc"
    9.16  
    9.17 -isatool keywords -t emacs \
    9.18 +isabelle keywords -t emacs \
    9.19    "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
    9.20    "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
    9.21  
    9.22 -isatool keywords -t emacs -k ZF \
    9.23 +isabelle keywords -t emacs -k ZF \
    9.24    "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
    9.25  
    9.26  
    9.27 @@ -25,6 +25,6 @@
    9.28  
    9.29  cd "$ISABELLE_HOME/lib/jedit"
    9.30  
    9.31 -isatool keywords -t jedit \
    9.32 +isabelle keywords -t jedit \
    9.33    "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz" \
    9.34    "$LOG/HOL-Statespace.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"

    10.1 --- a/INSTALL	Sat Oct 04 16:19:49 2008 +0200
    10.2 +++ b/INSTALL	Sat Oct 04 17:40:56 2008 +0200
    10.3 @@ -36,13 +36,13 @@
    10.4  The installation may be finished as follows:
    10.5  
    10.6    cd [ISABELLE_HOME]
    10.7 -  ./bin/isatool install -p /usr/local/bin
    10.8 +  ./bin/isabelle install -p /usr/local/bin
    10.9  
   10.10  The install utility creates global references to the present Isabelle
   10.11  installation, enabling users to invoke the Isabelle executables
   10.12 -without explicit path names.  Incidently, this is the only place where
   10.13 -a static reference to [ISABELLE_HOME] is created; thus isatool install
   10.14 -has to be run again whenever the Isabelle distribution is moved later.
   10.15 +without explicit path names.  This is the only place where a static
   10.16 +reference to [ISABELLE_HOME] is created; thus isabelle install has to
   10.17 +be run again whenever the Isabelle distribution is moved later.
   10.18  
   10.19  
   10.20  Compiling logics
   10.21 @@ -69,18 +69,18 @@
   10.22  Running the Isabelle binaries
   10.23  -----------------------------
   10.24  
   10.25 -Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
   10.26 -directly from their location within the distribution directory
   10.27 -[ISABELLE_HOME] like this:
   10.28 +Users may invoke the main Isabelle binaries (isabelle and
   10.29 +isabelle-process) directly from their location within the distribution
   10.30 +directory [ISABELLE_HOME] like this:
   10.31  
   10.32 -  [ISABELLE_HOME]/bin/isabelle HOL
   10.33 +  [ISABELLE_HOME]/bin/isabelle-process HOL
   10.34  
   10.35  This starts an interactive Isabelle session within the current text
   10.36  terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
   10.37  PATH.  An alternative is to create global references to the Isabelle
   10.38  executables as follows:
   10.39  
   10.40 -  [ISABELLE_HOME]/bin/isatool install -p ~/bin
   10.41 +  [ISABELLE_HOME]/bin/isabelle install -p ~/bin
   10.42  
   10.43  Note that the site-wide Isabelle installation may already provide
   10.44  Isabelle executables in some global bin directory (such as

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

    12.1 --- a/bin/isabelle	Sat Oct 04 16:19:49 2008 +0200
    12.2 +++ b/bin/isabelle	Sat Oct 04 17:40:56 2008 +0200
    12.3 @@ -3,23 +3,76 @@
    12.4  # $Id$
    12.5  # Author: Markus Wenzel, TU Muenchen
    12.6  #
    12.7 -# Smart selection of isabelle-process versus isabelle-interface.
    12.8 +# Isabelle tool wrapper.
    12.9  
   12.10  if [ -L "$0" ]; then
   12.11    TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
   12.12    exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
   12.13  fi
   12.14  
   12.15 -THIS=$(cd "$(dirname "$0")"; pwd -P)
   12.16 -NAME="$(basename "$0")"
   12.17  
   12.18 -case "$NAME" in
   12.19 -  I*)
   12.20 -    PRG=isabelle-interface
   12.21 -    ;;
   12.22 -  i*)
   12.23 -    PRG=isabelle-process
   12.24 -    ;;
   12.25 -esac
   12.26 +## settings
   12.27  
   12.28 -exec "$THIS/$PRG" "$@"
   12.29 +PRG="$(basename "$0")"
   12.30 +
   12.31 +ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
   12.32 +source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
   12.33 +
   12.34 +
   12.35 +## diagnostics
   12.36 +
   12.37 +function usage()
   12.38 +{
   12.39 +  echo
   12.40 +  echo "Usage: $PRG TOOL [ARGS ...]"
   12.41 +  echo
   12.42 +  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
   12.43 +  echo "  for more specific help."
   12.44 +  echo
   12.45 +  echo "  Available tools are:"
   12.46 +  (
   12.47 +    ORIG_IFS="$IFS"
   12.48 +    IFS=":"
   12.49 +    for DIR in $ISABELLE_TOOLS
   12.50 +    do
   12.51 +      cd "$DIR"
   12.52 +      for T in *
   12.53 +      do
   12.54 +        if [ -f "$T" -a -x "$T" ]; then
   12.55 +          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
   12.56 +          echo "    $T - $DESCRLINE"
   12.57 +        fi
   12.58 +      done
   12.59 +    done
   12.60 +    IFS="$ORIG_IFS"
   12.61 +  )
   12.62 +  exit 1
   12.63 +}
   12.64 +
   12.65 +function fail()
   12.66 +{
   12.67 +  echo "$1" >&2
   12.68 +  exit 2
   12.69 +}
   12.70 +
   12.71 +
   12.72 +## args
   12.73 +
   12.74 +[ "$#" -lt 1 -o "$1" = "-?" ] && usage
   12.75 +
   12.76 +TOOLNAME="$1"
   12.77 +shift
   12.78 +
   12.79 +
   12.80 +## main
   12.81 +
   12.82 +ORIG_IFS="$IFS"
   12.83 +IFS=":"
   12.84 +for DIR in $ISABELLE_TOOLS
   12.85 +do
   12.86 +  TOOL="$DIR/$TOOLNAME"
   12.87 +  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
   12.88 +done
   12.89 +IFS="$ORIG_IFS"
   12.90 +
   12.91 +fail "Unknown Isabelle tool: $TOOLNAME"

    13.1 --- a/bin/isatool	Sat Oct 04 16:19:49 2008 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,78 +0,0 @@
    13.4 -#!/usr/bin/env bash
    13.5 -#
    13.6 -# $Id$
    13.7 -# Author: Markus Wenzel, TU Muenchen
    13.8 -#
    13.9 -# Isabelle tool starter.
   13.10 -
   13.11 -if [ -L "$0" ]; then
   13.12 -  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
   13.13 -  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
   13.14 -fi
   13.15 -
   13.16 -
   13.17 -## settings
   13.18 -
   13.19 -PRG="$(basename "$0")"
   13.20 -
   13.21 -ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
   13.22 -source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
   13.23 -
   13.24 -
   13.25 -## diagnostics
   13.26 -
   13.27 -function usage()
   13.28 -{
   13.29 -  echo
   13.30 -  echo "Usage: $PRG TOOL [ARGS ...]"
   13.31 -  echo
   13.32 -  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
   13.33 -  echo "  for more specific help."
   13.34 -  echo
   13.35 -  echo "  Available tools are:"
   13.36 -  (
   13.37 -    ORIG_IFS="$IFS"
   13.38 -    IFS=":"
   13.39 -    for DIR in $ISABELLE_TOOLS
   13.40 -    do
   13.41 -      cd "$DIR"
   13.42 -      for T in *
   13.43 -      do
   13.44 -        if [ -f "$T" -a -x "$T" ]; then
   13.45 -          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
   13.46 -          echo "    $T - $DESCRLINE"
   13.47 -        fi
   13.48 -      done
   13.49 -    done
   13.50 -    IFS="$ORIG_IFS"
   13.51 -  )
   13.52 -  exit 1
   13.53 -}
   13.54 -
   13.55 -function fail()
   13.56 -{
   13.57 -  echo "$1" >&2
   13.58 -  exit 2
   13.59 -}
   13.60 -
   13.61 -
   13.62 -## args
   13.63 -
   13.64 -[ "$#" -lt 1 -o "$1" = "-?" ] && usage
   13.65 -
   13.66 -TOOLNAME="$1"
   13.67 -shift
   13.68 -
   13.69 -
   13.70 -## main
   13.71 -
   13.72 -ORIG_IFS="$IFS"
   13.73 -IFS=":"
   13.74 -for DIR in $ISABELLE_TOOLS
   13.75 -do
   13.76 -  TOOL="$DIR/$TOOLNAME"
   13.77 -  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
   13.78 -done
   13.79 -IFS="$ORIG_IFS"
   13.80 -
   13.81 -fail "Unknown Isabelle tool: $TOOLNAME"

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

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

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

    17.1 --- a/doc-src/System/Thy/Basics.thy	Sat Oct 04 16:19:49 2008 +0200
    17.2 +++ b/doc-src/System/Thy/Basics.thy	Sat Oct 04 17:40:56 2008 +0200
    17.3 @@ -22,22 +22,21 @@
    17.4    variables to all Isabelle programs (including tools and user
    17.5    interfaces).
    17.6  
    17.7 -  \item The \emph{raw Isabelle process} (@{executable_ref isabelle} or
    17.8 -  @{executable_ref "isabelle-process"}) runs logic sessions either
    17.9 -  interactively or in batch mode.  In particular, this view abstracts
   17.10 -  over the invocation of the actual ML system to be used.  Regular
   17.11 -  users rarely need to care about the low-level process.
   17.12 +  \item The \emph{raw Isabelle process} (@{executable_ref
   17.13 +  "isabelle-process"}) runs logic sessions either interactively or in
   17.14 +  batch mode.  In particular, this view abstracts over the invocation
   17.15 +  of the actual ML system to be used.  Regular users rarely need to
   17.16 +  care about the low-level process.
   17.17  
   17.18 -  \item The \emph{Isabelle tools wrapper} (@{executable_ref isatool})
   17.19 +  \item The \emph{Isabelle tools wrapper} (@{executable_ref isabelle})
   17.20    provides a generic startup environment Isabelle related utilities,
   17.21    user interfaces etc.  Such tools automatically benefit from the
   17.22    settings mechanism.
   17.23  
   17.24    \item The \emph{Isabelle interface wrapper} (@{executable_ref
   17.25 -  Isabelle} or @{executable_ref "isabelle-interface"}) provides some
   17.26 -  abstraction over the actual user interface to be used.  The de-facto
   17.27 -  standard interface for Isabelle is Proof~General
   17.28 -  \cite{proofgeneral}.
   17.29 +  "isabelle-interface"}) provides some abstraction over the actual
   17.30 +  user interface to be used.  The de-facto standard interface for
   17.31 +  Isabelle is Proof~General \cite{proofgeneral}.
   17.32  
   17.33    \end{enumerate}
   17.34  *}
   17.35 @@ -128,7 +127,7 @@
   17.36  
   17.37    \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
   17.38    automatically to the absolute path names of the @{executable
   17.39 -  "isabelle-process"} and @{executable isatool} executables,
   17.40 +  "isabelle-process"} and @{executable isabelle} executables,
   17.41    respectively.
   17.42    
   17.43    \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
   17.44 @@ -171,7 +170,7 @@
   17.45    \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
   17.46    ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   17.47    names of the @{executable "isabelle-process"} and @{executable
   17.48 -  isatool} executables, respectively.  Thus other tools and scripts
   17.49 +  isabelle} executables, respectively.  Thus other tools and scripts
   17.50    need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is
   17.51    on the current search path of the shell.
   17.52    
   17.53 @@ -234,8 +233,8 @@
   17.54    document preparation (see also \secref{sec:tool-latex}).
   17.55    
   17.56    \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
   17.57 -  directories that are scanned by @{executable isatool} for external
   17.58 -  utility programs (see also \secref{sec:isatool}).
   17.59 +  directories that are scanned by @{executable isabelle} for external
   17.60 +  utility programs (see also \secref{sec:isabelle-tool}).
   17.61    
   17.62    \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
   17.63    directories with documentation files.
   17.64 @@ -269,11 +268,10 @@
   17.65  section {* The raw Isabelle process *}
   17.66  
   17.67  text {*
   17.68 -  The @{executable_def isabelle} (or @{executable_def
   17.69 -  "isabelle-process"}) executable runs bare-bones Isabelle logic
   17.70 -  sessions --- either interactively or in batch mode.  It provides an
   17.71 -  abstraction over the underlying ML system, and over the actual heap
   17.72 -  file locations.  Its usage is:
   17.73 +  The @{executable_def "isabelle-process"} executable runs bare-bones
   17.74 +  Isabelle logic sessions --- either interactively or in batch mode.
   17.75 +  It provides an abstraction over the underlying ML system, and over
   17.76 +  the actual heap file locations.  Its usage is:
   17.77  
   17.78  \begin{ttbox}
   17.79  Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
   17.80 @@ -430,14 +428,14 @@
   17.81  *}
   17.82  
   17.83  
   17.84 -section {* The Isabelle tools wrapper \label{sec:isatool} *}
   17.85 +section {* The Isabelle tools wrapper \label{sec:isabelle-tool} *}
   17.86  
   17.87  text {*
   17.88    All Isabelle related tools and interfaces are called via a common
   17.89 -  wrapper --- @{executable isatool}:
   17.90 +  wrapper --- @{executable isabelle}:
   17.91  
   17.92  \begin{ttbox}
   17.93 -Usage: isatool TOOL [ARGS ...]
   17.94 +Usage: isabelle TOOL [ARGS ...]
   17.95  
   17.96    Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
   17.97    for more specific help.
   17.98 @@ -451,7 +449,7 @@
   17.99    In principle, Isabelle tools are ordinary executable scripts that
  17.100    are run within the Isabelle settings environment, see
  17.101    \secref{sec:settings}.  The set of available tools is collected by
  17.102 -  @{executable isatool} from the directories listed in the @{setting
  17.103 +  @{executable isabelle} from the directories listed in the @{setting
  17.104    ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
  17.105    from the shell.  Neither should you add the tool directories to your
  17.106    shell's search path!
  17.107 @@ -465,22 +463,22 @@
  17.108    installation like this:
  17.109  
  17.110  \begin{ttbox}
  17.111 -  isatool doc
  17.112 +  isabelle doc
  17.113  \end{ttbox}
  17.114  
  17.115    View a certain document as follows:
  17.116  \begin{ttbox}
  17.117 -  isatool doc isar-ref
  17.118 +  isabelle doc isar-ref
  17.119  \end{ttbox}
  17.120  
  17.121    Create an Isabelle session derived from HOL (see also
  17.122    \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
  17.123  \begin{ttbox}
  17.124 -  isatool mkdir HOL Test && isatool make
  17.125 +  isabelle mkdir HOL Test && isabelle make
  17.126  \end{ttbox}
  17.127 -  Note that @{verbatim "isatool mkdir"} is usually only invoked once;
  17.128 +  Note that @{verbatim "isabelle mkdir"} is usually only invoked once;
  17.129    existing sessions (including document output etc.) are then updated
  17.130 -  by @{verbatim "isatool make"} alone.
  17.131 +  by @{verbatim "isabelle make"} alone.
  17.132  *}
  17.133  
  17.134  

    18.1 --- a/doc-src/System/Thy/Misc.thy	Sat Oct 04 16:19:49 2008 +0200
    18.2 +++ b/doc-src/System/Thy/Misc.thy	Sat Oct 04 17:40:56 2008 +0200
    18.3 @@ -144,7 +144,7 @@
    18.4    Get the ML system name and the location where the compiler binaries
    18.5    are supposed to reside as follows:
    18.6  \begin{ttbox}
    18.7 -isatool getenv ML_SYSTEM ML_HOME
    18.8 +isabelle getenv ML_SYSTEM ML_HOME
    18.9  {\out ML_SYSTEM=polyml}
   18.10  {\out ML_HOME=/usr/share/polyml/x86-linux}
   18.11  \end{ttbox}
   18.12 @@ -152,7 +152,7 @@
   18.13    The next one peeks at the output directory for Isabelle logic
   18.14    images:
   18.15  \begin{ttbox}
   18.16 -isatool getenv -b ISABELLE_OUTPUT
   18.17 +isabelle getenv -b ISABELLE_OUTPUT
   18.18  {\out /home/me/isabelle/heaps/polyml_x86-linux}
   18.19  \end{ttbox}
   18.20    Here we have used the @{verbatim "-b"} option to suppress the
   18.21 @@ -171,11 +171,11 @@
   18.22  section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
   18.23  
   18.24  text {*
   18.25 -  By default, the Isabelle binaries (@{executable "isabelle-process"},
   18.26 -  @{executable isatool} etc.) are just run from their location within
   18.27 -  the distribution directory, probably indirectly by the shell through
   18.28 -  its @{setting PATH}.  Other schemes of installation are supported by
   18.29 -  the @{tool_def install} utility:
   18.30 +  By default, the main Isabelle binaries (@{executable "isabelle"}
   18.31 +  etc.)  are just run from their location within the distribution
   18.32 +  directory, probably indirectly by the shell through its @{setting
   18.33 +  PATH}.  Other schemes of installation are supported by the
   18.34 +  @{tool_def install} utility:
   18.35  \begin{ttbox}
   18.36  Usage: install [OPTIONS]
   18.37  
   18.38 @@ -192,7 +192,7 @@
   18.39    distribution directory as determined by @{setting ISABELLE_HOME}.
   18.40  
   18.41    The @{verbatim "-p"} option installs executable wrapper scripts for
   18.42 -  @{executable "isabelle-process"}, @{executable isatool},
   18.43 +  @{executable "isabelle-process"}, @{executable isabelle},
   18.44    @{executable Isabelle}, containing proper absolute references to the
   18.45    Isabelle distribution directory.  A typical @{verbatim DIR}
   18.46    specification would be some directory expected to be in the shell's
   18.47 @@ -218,7 +218,7 @@
   18.48      -q           quiet mode
   18.49  \end{ttbox}
   18.50    You are encouraged to use this to create a derived logo for your
   18.51 -  Isabelle project.  For example, @{verbatim isatool} @{tool
   18.52 +  Isabelle project.  For example, @{verbatim isabelle} @{tool
   18.53    logo}~@{verbatim Bali} creates @{verbatim isabelle_bali.eps}.
   18.54  *}
   18.55  
   18.56 @@ -267,7 +267,7 @@
   18.57  \begin{ttbox}
   18.58  Usage: makeall [ARGS ...]
   18.59  
   18.60 -  Apply isatool make to all logics (passing ARGS).
   18.61 +  Apply isabelle make to all logics (passing ARGS).
   18.62  \end{ttbox}
   18.63  
   18.64    The arguments @{verbatim ARGS} are just passed verbatim to each

    19.1 --- a/doc-src/System/Thy/Presentation.thy	Sat Oct 04 16:19:49 2008 +0200
    19.2 +++ b/doc-src/System/Thy/Presentation.thy	Sat Oct 04 17:40:56 2008 +0200
    19.3 @@ -28,24 +28,24 @@
    19.4    \begin{center}
    19.5    \begin{tabular}{lp{0.6\textwidth}}
    19.6  
    19.7 -      @{verbatim isatool} @{tool_ref mkdir} & invoked once by the user
    19.8 +      @{verbatim isabelle} @{tool_ref mkdir} & invoked once by the user
    19.9        to create the initial source setup (common @{verbatim
   19.10        IsaMakefile} plus a single session directory); \\
   19.11  
   19.12 -      @{verbatim isatool} @{tool make} & invoked repeatedly by the
   19.13 +      @{verbatim isabelle} @{tool make} & invoked repeatedly by the
   19.14        user to keep session output up-to-date (HTML, documents etc.); \\
   19.15  
   19.16 -      @{verbatim isatool} @{tool usedir} & part of the standard
   19.17 +      @{verbatim isabelle} @{tool usedir} & part of the standard
   19.18        @{verbatim IsaMakefile} entry of a session; \\
   19.19  
   19.20        @{executable "isabelle-process"} & run through @{verbatim
   19.21 -      isatool} @{tool_ref usedir}; \\
   19.22 +      isabelle} @{tool_ref usedir}; \\
   19.23  
   19.24 -      @{verbatim isatool} @{tool_ref document} & run by the Isabelle
   19.25 +      @{verbatim isabelle} @{tool_ref document} & run by the Isabelle
   19.26        process if document preparation is enabled; \\
   19.27  
   19.28 -      @{verbatim isatool} @{tool_ref latex} & universal {\LaTeX} tool
   19.29 -      wrapper invoked multiple times by @{verbatim isatool} @{tool_ref
   19.30 +      @{verbatim isabelle} @{tool_ref latex} & universal {\LaTeX} tool
   19.31 +      wrapper invoked multiple times by @{verbatim isabelle} @{tool_ref
   19.32        document}; also useful for manual experiments; \\
   19.33  
   19.34    \end{tabular}
   19.35 @@ -82,7 +82,7 @@
   19.36    The easiest way to let Isabelle generate theory browsing information
   19.37    for existing sessions is to append ``@{verbatim "-i true"}'' to the
   19.38    @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
   19.39 -  isatool} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
   19.40 +  isabelle} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
   19.41    example, add something like this to your Isabelle settings file
   19.42  
   19.43  \begin{ttbox}
   19.44 @@ -90,7 +90,7 @@
   19.45  \end{ttbox}
   19.46  
   19.47    and then change into the @{"file" "~~/src/FOL"} directory and run
   19.48 -  @{verbatim isatool} @{tool make}, or even @{verbatim isatool} @{tool
   19.49 +  @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
   19.50    make}~@{verbatim all}.  The presentation output will appear in
   19.51    @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
   19.52    @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
   19.53 @@ -130,19 +130,19 @@
   19.54    ISABELLE_BROWSER_INFO} to your WWW server, having generated browser
   19.55    info like this:
   19.56  \begin{ttbox}
   19.57 -isatool usedir -i true HOL Foo
   19.58 +isabelle usedir -i true HOL Foo
   19.59  \end{ttbox}
   19.60  
   19.61    This assumes that directory @{verbatim Foo} contains some @{verbatim
   19.62    ROOT.ML} file to load all your theories, and HOL is your parent
   19.63 -  logic image (@{verbatim isatool} @{tool_ref mkdir} assists in
   19.64 +  logic image (@{verbatim isabelle} @{tool_ref mkdir} assists in
   19.65    setting up Isabelle session directories.  Theory browser information
   19.66    for HOL should have been generated already beforehand.
   19.67    Alternatively, one may specify an external link to an existing body
   19.68    of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like
   19.69    this:
   19.70  \begin{ttbox}
   19.71 -isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
   19.72 +isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
   19.73  \end{ttbox}
   19.74  
   19.75    \medskip For production use, the @{tool usedir} tool is usually
   19.76 @@ -151,7 +151,7 @@
   19.77    provide easy setup of all this, with only minimal manual editing
   19.78    required.
   19.79  \begin{ttbox}
   19.80 -isatool mkdir HOL Foo && isatool make
   19.81 +isabelle mkdir HOL Foo && isabelle make
   19.82  \end{ttbox}
   19.83    See \secref{sec:tool-mkdir} for more information on preparing
   19.84    Isabelle session directories, including the setup for documents.
   19.85 @@ -169,7 +169,7 @@
   19.86    hidden, thus enabling the user to collapse irrelevant portions of
   19.87    information.  The browser is written in Java, it can be used both as
   19.88    a stand-alone application and as an applet.  Note that the option
   19.89 -  @{verbatim "-g"} of @{verbatim isatool} @{tool_ref usedir} creates
   19.90 +  @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates
   19.91    graph presentations in batch mode for inclusion in session
   19.92    documents.
   19.93  *}
   19.94 @@ -342,7 +342,7 @@
   19.95    directory with a minimal @{verbatim root.tex} that is sufficient to
   19.96    print all theories of the session (in the order of appearance); see
   19.97    \secref{sec:tool-document} for further information on Isabelle
   19.98 -  document preparation.  The usage of @{verbatim isatool} @{tool
   19.99 +  document preparation.  The usage of @{verbatim isabelle} @{tool
  19.100    mkdir} is:
  19.101  
  19.102  \begin{ttbox}
  19.103 @@ -406,12 +406,12 @@
  19.104    default logic, with proper document generation is generated like
  19.105    this:
  19.106  \begin{ttbox}
  19.107 -isatool mkdir Foo && isatool make
  19.108 +isabelle mkdir Foo && isabelle make
  19.109  \end{ttbox}
  19.110  
  19.111    \noindent The theory sources should be put into the @{verbatim Foo}
  19.112    directory, and its @{verbatim ROOT.ML} should be edited to load all
  19.113 -  required theories.  Invoking @{verbatim isatool} @{tool make} again
  19.114 +  required theories.  Invoking @{verbatim isabelle} @{tool make} again
  19.115    would run the whole session, generating browser information and the
  19.116    document automatically.  The @{verbatim IsaMakefile} is typically
  19.117    tuned manually later, e.g.\ adding source dependencies, or changing
  19.118 @@ -423,7 +423,7 @@
  19.119    meant to cover all of the sub-session directories at the same time
  19.120    (this is the deeper reasong why @{verbatim IsaMakefile} is not made
  19.121    part of the initial session directory created by @{verbatim
  19.122 -  isatool} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
  19.123 +  isabelle} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
  19.124    a full-blown example.
  19.125  *}
  19.126  
  19.127 @@ -546,10 +546,10 @@
  19.128    relative to the session's main directory.  If the @{verbatim "-C"}
  19.129    option is true, this will include a copy of an existing @{verbatim
  19.130    document} directory as provided by the user.  For example,
  19.131 -  @{verbatim isatool} @{tool usedir}~@{verbatim "-D generated HOL
  19.132 +  @{verbatim isabelle} @{tool usedir}~@{verbatim "-D generated HOL
  19.133    Foo"} produces a complete set of document sources at @{verbatim
  19.134    "Foo/generated"}.  Subsequent invocation of @{verbatim
  19.135 -  isatool} @{tool document}~@{verbatim "Foo/generated"} (see also
  19.136 +  isabelle} @{tool document}~@{verbatim "Foo/generated"} (see also
  19.137    \secref{sec:tool-document}) will process the final result
  19.138    independently of an Isabelle job.  This decoupled mode of operation
  19.139    facilitates debugging of serious {\LaTeX} errors, for example.
  19.140 @@ -697,7 +697,7 @@
  19.141    "~~/lib/texinputs/pdfsetup.sty"} as well.
  19.142  
  19.143    \medskip As a final step of document preparation within Isabelle,
  19.144 -  @{verbatim isatool} @{tool document}~@{verbatim "-c"} is run on the
  19.145 +  @{verbatim isabelle} @{tool document}~@{verbatim "-c"} is run on the
  19.146    resulting @{verbatim document} directory.  Thus the actual output
  19.147    document is built and installed in its proper place (as linked by
  19.148    the session's @{verbatim index.html} if option @{verbatim "-i"} of
  19.149 @@ -748,7 +748,7 @@
  19.150  subsubsection {* Examples *}
  19.151  
  19.152  text {*
  19.153 -  Invoking @{verbatim isatool} @{tool latex} by hand may be
  19.154 +  Invoking @{verbatim isabelle} @{tool latex} by hand may be
  19.155    occasionally useful when debugging failed attempts of the automatic
  19.156    document preparation stage of batch-mode Isabelle.  The abortive
  19.157    process leaves the sources at a certain place within @{setting
  19.158 @@ -757,7 +757,7 @@
  19.159    like this:
  19.160  \begin{ttbox}
  19.161    cd ~/isabelle/browser_info/HOL/Test/document
  19.162 -  isatool latex -o pdf
  19.163 +  isabelle latex -o pdf
  19.164  \end{ttbox}
  19.165  *}
  19.166  

    20.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Sat Oct 04 16:19:49 2008 +0200
    20.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Sat Oct 04 17:40:56 2008 +0200
    20.3 @@ -347,18 +347,18 @@
    20.4    (usually rooted at \verb,~/isabelle/browser_info,).
    20.5  
    20.6    \medskip The easiest way to manage Isabelle sessions is via
    20.7 -  \texttt{isatool mkdir} (generates an initial session source setup)
    20.8 -  and \texttt{isatool make} (run sessions controlled by
    20.9 +  \texttt{isabelle mkdir} (generates an initial session source setup)
   20.10 +  and \texttt{isabelle make} (run sessions controlled by
   20.11    \texttt{IsaMakefile}).  For example, a new session
   20.12    \texttt{MySession} derived from \texttt{HOL} may be produced as
   20.13    follows:
   20.14  
   20.15  \begin{verbatim}
   20.16 -  isatool mkdir HOL MySession
   20.17 -  isatool make
   20.18 +  isabelle mkdir HOL MySession
   20.19 +  isabelle make
   20.20  \end{verbatim}
   20.21  
   20.22 -  The \texttt{isatool make} job also informs about the file-system
   20.23 +  The \texttt{isabelle make} job also informs about the file-system
   20.24    location of the ultimate results.  The above dry run should be able
   20.25    to produce some \texttt{document.pdf} (with dummy title, empty table
   20.26    of contents etc.).  Any failure at this stage usually indicates
   20.27 @@ -394,7 +394,7 @@
   20.28    several sessions may be managed by the same \texttt{IsaMakefile}.
   20.29    See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
   20.30    for further details, especially on
   20.31 -  \texttt{isatool usedir} and \texttt{isatool make}.
   20.32 +  \texttt{isabelle usedir} and \texttt{isabelle make}.
   20.33  
   20.34    \end{itemize}
   20.35  
   20.36 @@ -417,7 +417,7 @@
   20.37    \texttt{MySession/document} directory as well.  In particular,
   20.38    adding a file named \texttt{root.bib} causes an automatic run of
   20.39    \texttt{bibtex} to process a bibliographic database; see also
   20.40 -  \texttt{isatool document} \cite{isabelle-sys}.
   20.41 +  \texttt{isabelle document} \cite{isabelle-sys}.
   20.42  
   20.43    \medskip Any failure of the document preparation phase in an
   20.44    Isabelle batch session leaves the generated sources in their target
   20.45 @@ -753,7 +753,7 @@
   20.46    tagged region, in order to keep, drop, or fold the corresponding
   20.47    parts of the document.  See the \emph{Isabelle System Manual}
   20.48    \cite{isabelle-sys} for further details, especially on
   20.49 -  \texttt{isatool usedir} and \texttt{isatool document}.
   20.50 +  \texttt{isabelle usedir} and \texttt{isabelle document}.
   20.51  
   20.52    Ignored material is specified by delimiting the original formal
   20.53    source with special source comments

    21.1 --- a/etc/settings	Sat Oct 04 16:19:49 2008 +0200
    21.2 +++ b/etc/settings	Sat Oct 04 17:40:56 2008 +0200
    21.3 @@ -82,7 +82,7 @@
    21.4  
    21.5  
    21.6  ###
    21.7 -### Interactive sessions (cf. isatool tty)
    21.8 +### Interactive sessions (cf. isabelle tty)
    21.9  ###
   21.10  
   21.11  ISABELLE_LINE_EDITOR=""
   21.12 @@ -91,7 +91,7 @@
   21.13  
   21.14  
   21.15  ###
   21.16 -### Batch sessions (cf. isatool usedir)
   21.17 +### Batch sessions (cf. isabelle usedir)
   21.18  ###
   21.19  
   21.20  ISABELLE_USEDIR_OPTIONS="-p 1 -v true -V outline=/proof,/ML"
   21.21 @@ -109,7 +109,7 @@
   21.22  
   21.23  
   21.24  ###
   21.25 -### Document preparation (cf. isatool latex/document)
   21.26 +### Document preparation (cf. isabelle latex/document)
   21.27  ###
   21.28  
   21.29  ISABELLE_LATEX="latex"

    22.1 --- a/lib/Tools/install	Sat Oct 04 16:19:49 2008 +0200
    22.2 +++ b/lib/Tools/install	Sat Oct 04 17:40:56 2008 +0200
    22.3 @@ -74,7 +74,7 @@
    22.4  if [ -n "$BINDIR" ]; then
    22.5    mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
    22.6  
    22.7 -  for NAME in isatool isabelle-process isabelle-interface
    22.8 +  for NAME in isabelle isabelle-process isabelle-interface
    22.9    do
   22.10      BIN="$BINDIR/$NAME"
   22.11      DIST="$DISTDIR/bin/$NAME"
   22.12 @@ -85,12 +85,4 @@
   22.13      echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
   22.14      chmod +x "$BIN"
   22.15    done
   22.16 -  for NAME in Isabelle isabelle
   22.17 -  do
   22.18 -    BIN="$BINDIR/$NAME"
   22.19 -    echo "installing $BIN"
   22.20 -    rm -f "$BIN"
   22.21 -    cp "$ISABELLE_HOME/bin/$NAME" "$BIN" || fail "Cannot write file: $BIN"
   22.22 -    chmod +x "$BIN"
   22.23 -  done
   22.24  fi

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

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

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

    26.1 --- a/lib/scripts/getsettings	Sat Oct 04 16:19:49 2008 +0200
    26.2 +++ b/lib/scripts/getsettings	Sat Oct 04 17:40:56 2008 +0200
    26.3 @@ -20,7 +20,7 @@
    26.4  
    26.5  #key executables
    26.6  ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    26.7 -ISABELLE_TOOL="$ISABELLE_HOME/bin/isatool"
    26.8 +ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
    26.9  #legacy settings
   26.10  ISABELLE="$ISABELLE_PROCESS"
   26.11  ISATOOL="$ISABELLE_TOOL"

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

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

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

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

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

    32.1 --- a/src/Pure/README	Sat Oct 04 16:19:49 2008 +0200
    32.2 +++ b/src/Pure/README	Sat Oct 04 17:40:56 2008 +0200
    32.3 @@ -6,16 +6,16 @@
    32.4  is the basis for all object-logics.  The Isabelle/Pure image may be
    32.5  compiled in batch mode like this:
    32.6  
    32.7 -  isatool make Pure
    32.8 +  isabelle make Pure
    32.9  
   32.10  Developers may want to produce a RAW image that merely consists of the
   32.11  ML compiler with the compatibility setup of ML-Systems/ preloaded:
   32.12  
   32.13 -  isatool make RAW
   32.14 +  isabelle make RAW
   32.15  
   32.16  Now the Pure session may be compiled interactively as follows:
   32.17  
   32.18 -  isabelle -u RAW
   32.19 +  isabelle-process -u RAW
   32.20  
   32.21  See ROOT.ML for further information.
   32.22