1.1 --- a/Admin/Benchmarks/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
     1.2 +++ b/Admin/Benchmarks/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
     1.3 @@ -20,14 +20,14 @@
     1.4  ## HOL-datatype
     1.5  
     1.6  HOL:
     1.7 -	@cd $(SRC)/HOL; $(ISATOOL) make HOL
     1.8 +	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
     1.9  
    1.10  HOL-datatype: HOL $(LOG)/HOL-datatype.gz
    1.11  
    1.12  $(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/Brackin.thy \
    1.13    HOL-datatype/Instructions.thy HOL-datatype/SML.thy \
    1.14    HOL-datatype/Verilog.thy
    1.15 -	@$(ISATOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype
    1.16 +	@$(ISABELLE_TOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype
    1.17  
    1.18  
    1.19  ## clean

     2.1 --- a/Admin/build	Sat Oct 04 16:05:08 2008 +0200
     2.2 +++ b/Admin/build	Sat Oct 04 16:05:09 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 -  ISATOOL="$ISABELLE_DIR/Distribution/bin/isatool"
     2.8 +  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isatool"
     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 -  ISATOOL="$ISABELLE_DIR/bin/isatool"
    2.14 +  ISABELLE_TOOL="$ISABELLE_DIR/bin/isatool"
    2.15    ISABELLE_LIB="$ISABELLE_DIR/lib"
    2.16    ISABELLE_SRC="$ISABELLE_DIR/src"
    2.17    ISABELLE_DOC_SRC="$ISABELLE_DIR/doc-src"
    2.18 @@ -112,7 +112,7 @@
    2.19    type -p scalac >/dev/null || fail "Scala compiler unavailable"
    2.20  
    2.21    pushd "$ISABELLE_SRC/Pure" >/dev/null
    2.22 -  "$ISATOOL" make jar || fail "Failed to build Pure.jar!"
    2.23 +  "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
    2.24    popd >/dev/null
    2.25  
    2.26    if [ -d "$HOME/lib/jedit/current" ]; then

     3.1 --- a/Admin/isatest/isatest-annomaly	Sat Oct 04 16:05:08 2008 +0200
     3.2 +++ b/Admin/isatest/isatest-annomaly	Sat Oct 04 16:05:09 2008 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4  ## main
     3.5  
     3.6  ISABELLE_HOME="$DISTPREFIX/Isabelle"
     3.7 -ISATOOL="$ISABELLE_HOME/bin/isatool"
     3.8 +ISABELLE_TOOL="$ISABELLE_HOME/bin/isatool"
     3.9  
    3.10  [ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
    3.11  
    3.12 @@ -73,7 +73,7 @@
    3.13  do
    3.14    ( cd "$ISABELLE_HOME/src/$L"; \
    3.15      cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
    3.16 -    "$ISATOOL" make || fail "isatool make for $L failed." )
    3.17 +    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
    3.18  done
    3.19  
    3.20  

     4.1 --- a/Admin/isatest/isatest-doc	Sat Oct 04 16:05:08 2008 +0200
     4.2 +++ b/Admin/isatest/isatest-doc	Sat Oct 04 16:05:09 2008 +0200
     4.3 @@ -25,7 +25,7 @@
     4.4  SHORT=at-poly
     4.5  SETTINGS=~/settings/$SHORT
     4.6  
     4.7 -ISATOOL=$ISABELLE_DEVEL/bin/isatool
     4.8 +ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isatool
     4.9      
    4.10  
    4.11  MAIL=$HOME/bin/pmail
    4.12 @@ -80,7 +80,7 @@
    4.13      (
    4.14        cd $DIR
    4.15        ulimit -t $MAXTIME 
    4.16 -      nice $ISATOOL make >> $LOG 2>&1
    4.17 +      nice $ISABELLE_TOOL make >> $LOG 2>&1
    4.18      ) || FAIL="${FAIL}${DIR} "    
    4.19      echo "Finished [$DIR]" >> $LOG
    4.20      echo >> $LOG

     5.1 --- a/Admin/isatest/isatest-makeall	Sat Oct 04 16:05:08 2008 +0200
     5.2 +++ b/Admin/isatest/isatest-makeall	Sat Oct 04 16:05:09 2008 +0200
     5.3 @@ -88,9 +88,9 @@
     5.4          ;;
     5.5  esac
     5.6  
     5.7 -ISATOOL="$DISTPREFIX/Isabelle/bin/isatool"
     5.8 +ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isatool"
     5.9  
    5.10 -[ -x $ISATOOL ] || fail "Cannot run $ISATOOL"
    5.11 +[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
    5.12  
    5.13  if [ "$1" = "-l" ]; then
    5.14    shift
    5.15 @@ -98,12 +98,12 @@
    5.16    LOGIC="$1"
    5.17    TARGETS="$2"
    5.18    shift 2
    5.19 -  ISABELLE_HOME="$($ISATOOL getenv -b ISABELLE_HOME)"
    5.20 +  ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
    5.21    DIR="$ISABELLE_HOME/src/$LOGIC"
    5.22 -  TOOL="$ISATOOL make $MFLAGS $TARGETS"
    5.23 +  TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
    5.24  else
    5.25    DIR="."
    5.26 -  TOOL="$ISATOOL makeall $MFLAGS all"
    5.27 +  TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
    5.28  fi
    5.29  
    5.30  # main test loop

     6.1 --- a/build	Sat Oct 04 16:05:08 2008 +0200
     6.2 +++ b/build	Sat Oct 04 16:05:09 2008 +0200
     6.3 @@ -175,7 +175,7 @@
     6.4  
     6.5  for L in $MAKE_LOGICS
     6.6  do
     6.7 -  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
     6.8 +  ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make $TARGETS )
     6.9  done
    6.10  
    6.11  echo -n "Finished at "; date

     7.1 --- a/doc-src/AxClass/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
     7.2 +++ b/doc-src/AxClass/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
     7.3 @@ -13,7 +13,7 @@
     7.4  SRC = $(ISABELLE_HOME)/src
     7.5  OUT = $(ISABELLE_OUTPUT)
     7.6  LOG = $(OUT)/log
     7.7 -USEDIR = $(ISATOOL) usedir -d false -D document
     7.8 +USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
     7.9  
    7.10  
    7.11  ## Group
    7.12 @@ -21,7 +21,7 @@
    7.13  Group: HOL $(LOG)/HOL-Group.gz
    7.14  
    7.15  HOL:
    7.16 -	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    7.17 +	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
    7.18  
    7.19  $(LOG)/HOL-Group.gz: $(OUT)/HOL Group/ROOT.ML Group/Group.thy \
    7.20    Group/Product.thy Group/Semigroups.thy
    7.21 @@ -34,7 +34,7 @@
    7.22  Nat: FOL $(LOG)/FOL-Nat.gz
    7.23  
    7.24  FOL:
    7.25 -	@cd $(SRC)/FOL; $(ISATOOL) make FOL
    7.26 +	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
    7.27  
    7.28  $(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.thy
    7.29  	@$(USEDIR) $(OUT)/FOL Nat

     8.1 --- a/doc-src/IsarAdvanced/Classes/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
     8.2 +++ b/doc-src/IsarAdvanced/Classes/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4  OUT = $(ISABELLE_OUTPUT)
     8.5  LOG = $(OUT)/log
     8.6  
     8.7 -USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
     8.8 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
     8.9  
    8.10  
    8.11  ## Thy

     9.1 --- a/doc-src/IsarAdvanced/Codegen/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
     9.2 +++ b/doc-src/IsarAdvanced/Codegen/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
     9.3 @@ -14,7 +14,7 @@
     9.4  OUT = $(ISABELLE_OUTPUT)
     9.5  LOG = $(OUT)/log
     9.6  
     9.7 -USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
     9.8 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
     9.9  
    9.10  
    9.11  ## Thy

    10.1 --- a/doc-src/IsarAdvanced/Functions/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    10.2 +++ b/doc-src/IsarAdvanced/Functions/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    10.3 @@ -14,7 +14,7 @@
    10.4  OUT = $(ISABELLE_OUTPUT)
    10.5  LOG = $(OUT)/log
    10.6  
    10.7 -USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    10.8 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    10.9  
   10.10  
   10.11  ## Thy

    11.1 --- a/doc-src/IsarImplementation/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    11.2 +++ b/doc-src/IsarImplementation/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    11.3 @@ -14,7 +14,7 @@
    11.4  OUT = $(ISABELLE_OUTPUT)
    11.5  LOG = $(OUT)/log
    11.6  
    11.7 -USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    11.8 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    11.9  
   11.10  
   11.11  ## Thy

    12.1 --- a/doc-src/IsarOverview/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    12.2 +++ b/doc-src/IsarOverview/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    12.3 @@ -7,7 +7,7 @@
    12.4  SRC = $(ISABELLE_HOME)/src
    12.5  OUT = $(ISABELLE_OUTPUT)
    12.6  LOG = $(OUT)/log
    12.7 -USEDIR = $(ISATOOL) usedir -i false -g false -d false -D document -v true
    12.8 +USEDIR = $(ISABELLE_TOOL) usedir -i false -g false -d false -D document -v true
    12.9  
   12.10  
   12.11  ## Isar

    13.1 --- a/doc-src/IsarRef/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    13.2 +++ b/doc-src/IsarRef/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    13.3 @@ -14,7 +14,7 @@
    13.4  OUT = $(ISABELLE_OUTPUT)
    13.5  LOG = $(OUT)/log
    13.6  
    13.7 -USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    13.8 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    13.9  
   13.10  
   13.11  ## IsarRef sessions

    14.1 --- a/doc-src/LaTeXsugar/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    14.2 +++ b/doc-src/LaTeXsugar/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    14.3 @@ -14,7 +14,7 @@
    14.4  OUT = $(ISABELLE_OUTPUT)
    14.5  LOG = $(OUT)/log
    14.6  
    14.7 -USEDIR = $(ISATOOL) usedir -v true -i false -g false -d false -D document
    14.8 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -g false -d false -D document
    14.9  
   14.10  
   14.11  ## Sugar

    15.1 --- a/doc-src/Locales/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    15.2 +++ b/doc-src/Locales/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    15.3 @@ -13,7 +13,7 @@
    15.4  SRC = $(ISABELLE_HOME)/src
    15.5  OUT = $(ISABELLE_OUTPUT)
    15.6  LOG = $(OUT)/log
    15.7 -USEDIR = $(ISATOOL) usedir -d false -D document
    15.8 +USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
    15.9  
   15.10  
   15.11  ## Locales
   15.12 @@ -21,7 +21,7 @@
   15.13  Locales: $(LOG)/HOL-Locales.gz
   15.14  
   15.15  HOL:
   15.16 -	@cd $(SRC)/HOL; $(ISATOOL) make HOL
   15.17 +	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
   15.18  
   15.19  $(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Examples.thy \
   15.20    Locales/Examples1.thy Locales/Examples2.thy Locales/Examples3.thy \

    16.1 --- a/doc-src/System/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    16.2 +++ b/doc-src/System/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    16.3 @@ -14,7 +14,7 @@
    16.4  OUT = $(ISABELLE_OUTPUT)
    16.5  LOG = $(OUT)/log
    16.6  
    16.7 -USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    16.8 +USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
    16.9  
   16.10  
   16.11  ## IsarRef sessions

    17.1 --- a/doc-src/System/Thy/Basics.thy	Sat Oct 04 16:05:08 2008 +0200
    17.2 +++ b/doc-src/System/Thy/Basics.thy	Sat Oct 04 16:05:09 2008 +0200
    17.3 @@ -126,7 +126,7 @@
    17.4  
    17.5    \begin{itemize}
    17.6  
    17.7 -  \item @{setting_def ISABELLE} and @{setting_def ISATOOL} are set
    17.8 +  \item @{setting_def ISABELLE} and @{setting_def ISABELLE_TOOL} are set
    17.9    automatically to the absolute path names of the @{executable
   17.10    "isabelle-process"} and @{executable isatool} executables,
   17.11    respectively.
   17.12 @@ -169,7 +169,7 @@
   17.13    a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
   17.14    
   17.15    \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting
   17.16 -  ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path
   17.17 +  ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   17.18    names of the @{executable "isabelle-process"} and @{executable
   17.19    isatool} executables, respectively.  Thus other tools and scripts
   17.20    need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is

    18.1 --- a/doc-src/TutorialI/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    18.2 +++ b/doc-src/TutorialI/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    18.3 @@ -18,19 +18,19 @@
    18.4  OUT = $(ISABELLE_OUTPUT)
    18.5  LOG = $(OUT)/log
    18.6  OPTIONS = -m brackets -i true -d "" -D document
    18.7 -USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL
    18.8 +USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/HOL
    18.9  
   18.10  
   18.11  ## HOL
   18.12  
   18.13  HOL:
   18.14 -	@cd $(SRC)/HOL; $(ISATOOL) make HOL
   18.15 +	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
   18.16  
   18.17  styles:
   18.18  	@rm -f isabelle.sty
   18.19  	@rm -f isabellesym.sty
   18.20  	@rm -f pdfsetup.sty
   18.21 -	@$(ISATOOL) latex -o sty >/dev/null
   18.22 +	@$(ISABELLE_TOOL) latex -o sty >/dev/null
   18.23  	@rm -f pdfsetup.sty
   18.24  	@rm -f */document/isabelle.sty
   18.25  	@rm -f */document/isabellesym.sty

    19.1 --- a/doc-src/TutorialI/Overview/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    19.2 +++ b/doc-src/TutorialI/Overview/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    19.3 @@ -7,7 +7,7 @@
    19.4  SRC = $(ISABELLE_HOME)/src
    19.5  OUT = $(ISABELLE_OUTPUT)
    19.6  LOG = $(OUT)/log
    19.7 -USEDIR = $(ISATOOL) usedir -i true -d ps -D document -v true
    19.8 +USEDIR = $(ISABELLE_TOOL) usedir -i true -d ps -D document -v true
    19.9  
   19.10  
   19.11  ## LNCS

    20.1 --- a/doc-src/ZF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    20.2 +++ b/doc-src/ZF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    20.3 @@ -16,19 +16,19 @@
    20.4  OUT = $(ISABELLE_OUTPUT)
    20.5  LOG = $(OUT)/log
    20.6  OPTIONS = -m brackets -i true -d "" -D document
    20.7 -USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/ZF
    20.8 +USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/ZF
    20.9  
   20.10  
   20.11  ## ZF
   20.12  
   20.13  ZF:
   20.14 -	@cd $(SRC)/ZF; $(ISATOOL) make ZF
   20.15 +	@cd $(SRC)/ZF; $(ISABELLE_TOOL) make ZF
   20.16  
   20.17  styles:
   20.18  	@rm -f isabelle.sty
   20.19  	@rm -f isabellesym.sty
   20.20  	@rm -f pdfsetup.sty
   20.21 -	@$(ISATOOL) latex -o sty >/dev/null
   20.22 +	@$(ISABELLE_TOOL) latex -o sty >/dev/null
   20.23  	@rm -f pdfsetup.sty
   20.24  	@rm -f document/isabelle.sty
   20.25  	@rm -f document/isabellesym.sty

    21.1 --- a/lib/Tools/browser	Sat Oct 04 16:05:08 2008 +0200
    21.2 +++ b/lib/Tools/browser	Sat Oct 04 16:05:09 2008 +0200
    21.3 @@ -65,7 +65,7 @@
    21.4  
    21.5  if [ -z "$GRAPHFILE" ]; then
    21.6    [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
    21.7 -  exec "$ISATOOL" java GraphBrowser.GraphBrowser
    21.8 +  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
    21.9  else
   21.10    PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
   21.11    if [ -n "$CLEAN" ]; then
   21.12 @@ -83,9 +83,9 @@
   21.13    esac
   21.14  
   21.15    if [ -z "$OUTFILE" ]; then
   21.16 -    "$ISATOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
   21.17 +    "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
   21.18    else
   21.19 -    "$ISATOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
   21.20 +    "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
   21.21    fi
   21.22    RC="$?"
   21.23  

    22.1 --- a/lib/Tools/doc	Sat Oct 04 16:05:08 2008 +0200
    22.2 +++ b/lib/Tools/doc	Sat Oct 04 16:05:09 2008 +0200
    22.3 @@ -53,7 +53,7 @@
    22.4      [ -d "$DIR" ] || fail "Bad document directory: $DIR"
    22.5      for FMT in "$ISABELLE_DOC_FORMAT" dvi
    22.6      do
    22.7 -      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; }
    22.8 +      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
    22.9      done
   22.10    done
   22.11    IFS="$ORIG_IFS"

    23.1 --- a/lib/Tools/document	Sat Oct 04 16:05:08 2008 +0200
    23.2 +++ b/lib/Tools/document	Sat Oct 04 16:05:09 2008 +0200
    23.3 @@ -119,11 +119,11 @@
    23.4  {
    23.5    local FMT="$1"
    23.6    [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
    23.7 -  "$ISATOOL" latex -o sty && \
    23.8 -  "$ISATOOL" latex -o "$FMT" && \
    23.9 -  { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
   23.10 -  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \
   23.11 -  "$ISATOOL" latex -o "$FMT"
   23.12 +  "$ISABELLE_TOOL" latex -o sty && \
   23.13 +  "$ISABELLE_TOOL" latex -o "$FMT" && \
   23.14 +  { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
   23.15 +  { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
   23.16 +  "$ISABELLE_TOOL" latex -o "$FMT"
   23.17  }
   23.18  
   23.19  (
   23.20 @@ -134,15 +134,15 @@
   23.21    prep_tags
   23.22  
   23.23    if [ -f IsaMakefile ]; then
   23.24 -    "$ISATOOL" make "$OUTFORMAT"
   23.25 +    "$ISABELLE_TOOL" make "$OUTFORMAT"
   23.26      RC="$?"
   23.27    elif [ "$OUTFORMAT" = pdf ]; then
   23.28      pre_latex pdf && \
   23.29 -    "$ISATOOL" latex -o pdf
   23.30 +    "$ISABELLE_TOOL" latex -o pdf
   23.31      RC="$?"
   23.32    else
   23.33      pre_latex dvi && \
   23.34 -    "$ISATOOL" latex -o "$OUTFORMAT"
   23.35 +    "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
   23.36      RC="$?"
   23.37    fi
   23.38  

    24.1 --- a/lib/Tools/makeall	Sat Oct 04 16:05:08 2008 +0200
    24.2 +++ b/lib/Tools/makeall	Sat Oct 04 16:05:09 2008 +0200
    24.3 @@ -41,7 +41,7 @@
    24.4  
    24.5  for L in $ALL_LOGICS
    24.6  do
    24.7 -  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L "
    24.8 +  ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$L "
    24.9  done
   24.10  
   24.11  echo -n "Finished at "; date

    25.1 --- a/lib/Tools/mkdir	Sat Oct 04 16:05:08 2008 +0200
    25.2 +++ b/lib/Tools/mkdir	Sat Oct 04 16:05:09 2008 +0200
    25.3 @@ -137,7 +137,7 @@
    25.4      echo "OUT = \$(ISABELLE_OUTPUT)"
    25.5      echo "LOG = \$(OUT)/log"
    25.6      echo
    25.7 -    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
    25.8 +    echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
    25.9      echo
   25.10      echo
   25.11      echo "## $NAME"
   25.12 @@ -146,7 +146,7 @@
   25.13        echo "$NAME: $LOGIC $TARGET"
   25.14        echo
   25.15        echo "$LOGIC:"
   25.16 -      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
   25.17 +      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) make $LOGIC"
   25.18        echo
   25.19        echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES"
   25.20        echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"

    26.1 --- a/lib/Tools/mkproject	Sat Oct 04 16:05:08 2008 +0200
    26.2 +++ b/lib/Tools/mkproject	Sat Oct 04 16:05:09 2008 +0200
    26.3 @@ -22,6 +22,5 @@
    26.4    usage
    26.5  fi
    26.6  
    26.7 -"$ISATOOL" mkdir -b -q "$NAME"
    26.8 -(cd document; "$ISATOOL" latex -o sty)
    26.9 -
   26.10 +"$ISABELLE_TOOL" mkdir -b -q "$NAME"
   26.11 +( cd document; "$ISABELLE_TOOL" latex -o sty; )

    27.1 --- a/src/CCL/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    27.2 +++ b/src/CCL/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    27.3 @@ -24,13 +24,13 @@
    27.4  CCL: FOL $(OUT)/CCL
    27.5  
    27.6  FOL:
    27.7 -	@cd $(SRC)/FOL; $(ISATOOL) make FOL
    27.8 +	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
    27.9  
   27.10  $(OUT)/FOL: FOL
   27.11  
   27.12  $(OUT)/CCL: $(OUT)/FOL CCL.thy Fix.thy Gfp.thy Hered.thy Lfp.thy ROOT.ML \
   27.13    Set.thy Term.thy Trancl.thy Type.thy Wfd.thy
   27.14 -	@$(ISATOOL) usedir -b -r $(OUT)/FOL CCL
   27.15 +	@$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL CCL
   27.16  
   27.17  
   27.18  ## CCL-ex
   27.19 @@ -39,7 +39,7 @@
   27.20  
   27.21  $(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.thy ex/List.thy ex/Nat.thy ex/ROOT.ML \
   27.22    ex/Stream.thy
   27.23 -	@$(ISATOOL) usedir $(OUT)/CCL ex
   27.24 +	@$(ISABELLE_TOOL) usedir $(OUT)/CCL ex
   27.25  
   27.26  
   27.27  ## clean

    28.1 --- a/src/CTT/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    28.2 +++ b/src/CTT/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    28.3 @@ -24,11 +24,11 @@
    28.4  CTT: Pure $(OUT)/CTT
    28.5  
    28.6  Pure:
    28.7 -	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    28.8 +	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    28.9  
   28.10  $(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
   28.11    Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
   28.12 -	@$(ISATOOL) usedir -b $(OUT)/Pure CTT
   28.13 +	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT
   28.14  
   28.15  
   28.16  ## CTT-ex
   28.17 @@ -37,7 +37,7 @@
   28.18  
   28.19  $(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
   28.20    ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
   28.21 -	@$(ISATOOL) usedir $(OUT)/CTT ex
   28.22 +	@$(ISABELLE_TOOL) usedir $(OUT)/CTT ex
   28.23  
   28.24  
   28.25  ## clean

    29.1 --- a/src/Cube/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    29.2 +++ b/src/Cube/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    29.3 @@ -24,10 +24,10 @@
    29.4  Pure-Cube: Pure $(LOG)/Pure-Cube.gz
    29.5  
    29.6  Pure:
    29.7 -	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    29.8 +	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    29.9  
   29.10  $(LOG)/Pure-Cube.gz: $(OUT)/Pure Cube.thy Example.thy ROOT.ML
   29.11 -	@cd ..; $(ISATOOL) usedir $(OUT)/Pure Cube
   29.12 +	@cd ..; $(ISABELLE_TOOL) usedir $(OUT)/Pure Cube
   29.13  
   29.14  
   29.15  ## clean

    30.1 --- a/src/FOL/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    30.2 +++ b/src/FOL/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    30.3 @@ -24,7 +24,7 @@
    30.4  FOL: Pure $(OUT)/FOL
    30.5  
    30.6  Pure:
    30.7 -	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    30.8 +	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    30.9  
   30.10  $(OUT)/Pure: Pure
   30.11  
   30.12 @@ -38,7 +38,7 @@
   30.13    $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.thy	\
   30.14    IFOL.thy ROOT.ML blastdata.ML cladata.ML document/root.tex		\
   30.15    fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
   30.16 -	@$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL
   30.17 +	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
   30.18  
   30.19  
   30.20  ## FOL-ex
   30.21 @@ -51,7 +51,7 @@
   30.22    ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
   30.23    ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy	\
   30.24    ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
   30.25 -	@$(ISATOOL) usedir $(OUT)/FOL ex
   30.26 +	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
   30.27  
   30.28  
   30.29  ## clean

    31.1 --- a/src/FOLP/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    31.2 +++ b/src/FOLP/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    31.3 @@ -24,11 +24,11 @@
    31.4  FOLP: Pure $(OUT)/FOLP
    31.5  
    31.6  Pure:
    31.7 -	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    31.8 +	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    31.9  
   31.10  $(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML	\
   31.11    hypsubst.ML intprover.ML simp.ML simpdata.ML
   31.12 -	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
   31.13 +	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP
   31.14  
   31.15  
   31.16  ## FOLP-ex
   31.17 @@ -40,7 +40,7 @@
   31.18    ex/Prolog.ML ex/Prolog.thy ex/Propositional_Int.thy			\
   31.19    ex/Propositional_Cla.thy ex/Quantifiers_Int.thy			\
   31.20    ex/Quantifiers_Cla.thy
   31.21 -	@$(ISATOOL) usedir $(OUT)/FOLP ex
   31.22 +	@$(ISABELLE_TOOL) usedir $(OUT)/FOLP ex
   31.23  
   31.24  
   31.25  ## clean

    32.1 --- a/src/HOL/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    32.2 +++ b/src/HOL/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    32.3 @@ -69,7 +69,7 @@
    32.4  HOL-Main: Pure $(OUT)/HOL-Main
    32.5  
    32.6  Pure:
    32.7 -	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    32.8 +	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    32.9  
   32.10  $(OUT)/Pure: Pure
   32.11  
   32.12 @@ -182,7 +182,7 @@
   32.13    $(SRC)/Tools/rat.ML
   32.14  
   32.15  $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
   32.16 -	@$(ISATOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
   32.17 +	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
   32.18  
   32.19  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
   32.20    Arith_Tools.thy \
   32.21 @@ -247,7 +247,7 @@
   32.22    Tools/TFL/utils.ML
   32.23  
   32.24  $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
   32.25 -	@$(ISATOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
   32.26 +	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
   32.27  
   32.28  $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
   32.29    Complex/Complex_Main.thy \
   32.30 @@ -285,7 +285,7 @@
   32.31    Tools/Qelim/ferrante_rackoff.ML \
   32.32    Tools/Qelim/langford_data.ML \
   32.33    Tools/Qelim/langford.ML
   32.34 -	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
   32.35 +	@$(ISABELLE_TOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
   32.36  
   32.37  
   32.38  ## HOL-Library
   32.39 @@ -320,7 +320,7 @@
   32.40    Library/Assert.thy Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
   32.41    Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
   32.42    Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
   32.43 -	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
   32.44 +	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
   32.45  
   32.46  
   32.47  ## HOL-HahnBanach
   32.48 @@ -337,7 +337,7 @@
   32.49    Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
   32.50    Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
   32.51    Real/HahnBanach/document/root.tex
   32.52 -	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL HahnBanach
   32.53 +	@cd Real; $(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
   32.54  
   32.55  
   32.56  ## HOL-Subst
   32.57 @@ -346,7 +346,7 @@
   32.58  
   32.59  $(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML		\
   32.60    Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
   32.61 -	@$(ISATOOL) usedir $(OUT)/HOL Subst
   32.62 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
   32.63  
   32.64  
   32.65  ## HOL-Induct
   32.66 @@ -359,7 +359,7 @@
   32.67    Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
   32.68    Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy		\
   32.69    Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
   32.70 -	@$(ISATOOL) usedir $(OUT)/HOL Induct
   32.71 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
   32.72  
   32.73  
   32.74  ## HOL-IMP
   32.75 @@ -370,7 +370,7 @@
   32.76    IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy	\
   32.77    IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy	\
   32.78    IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
   32.79 -	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP
   32.80 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
   32.81  
   32.82  
   32.83  ## HOL-IMPP
   32.84 @@ -379,7 +379,7 @@
   32.85  
   32.86  $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy		\
   32.87    IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
   32.88 -	@$(ISATOOL) usedir $(OUT)/HOL IMPP
   32.89 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
   32.90  
   32.91  
   32.92  ## HOL-Import
   32.93 @@ -397,7 +397,7 @@
   32.94  HOL-Import: HOL $(LOG)/HOL-Import.gz
   32.95  
   32.96  $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
   32.97 -	@$(ISATOOL) usedir $(OUT)/HOL Import
   32.98 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import
   32.99  
  32.100  
  32.101  ## HOL-Generate-HOL
  32.102 @@ -410,7 +410,7 @@
  32.103    Import/Generate-HOL/GenHOL4Real.thy					\
  32.104    Import/Generate-HOL/GenHOL4Vec.thy					\
  32.105    Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
  32.106 -	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOL
  32.107 +	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL
  32.108  
  32.109  
  32.110  ## HOL-Generate-HOLLight
  32.111 @@ -420,7 +420,7 @@
  32.112  $(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL		\
  32.113    $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy	\
  32.114    Import/Generate-HOLLight/ROOT.ML
  32.115 -	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOLLight
  32.116 +	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
  32.117  
  32.118  
  32.119  ## HOL-Import-HOL
  32.120 @@ -443,14 +443,14 @@
  32.121    Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy			\
  32.122    Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy	\
  32.123    Import/HOL/ROOT.ML
  32.124 -	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL HOL4
  32.125 +	@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4
  32.126  
  32.127  HOLLight: HOL $(LOG)/HOLLight.gz
  32.128  
  32.129  $(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES)	\
  32.130    Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy		\
  32.131    Import/HOLLight/ROOT.ML
  32.132 -	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL HOLLight
  32.133 +	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
  32.134  
  32.135  
  32.136  ## HOL-NumberTheory
  32.137 @@ -468,7 +468,7 @@
  32.138    NumberTheory/Euler.thy NumberTheory/Gauss.thy				\
  32.139    NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
  32.140    NumberTheory/ROOT.ML
  32.141 -	@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
  32.142 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NumberTheory
  32.143  
  32.144  
  32.145  ## HOL-Hoare
  32.146 @@ -481,7 +481,7 @@
  32.147    Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
  32.148    Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy	\
  32.149    Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
  32.150 -	@$(ISATOOL) usedir $(OUT)/HOL Hoare
  32.151 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
  32.152  
  32.153  
  32.154  ## HOL-HoareParallel
  32.155 @@ -498,7 +498,7 @@
  32.156    HoareParallel/RG_Syntax.thy HoareParallel/RG_Tran.thy			\
  32.157    HoareParallel/ROOT.ML HoareParallel/document/root.tex			\
  32.158    HoareParallel/document/root.bib
  32.159 -	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
  32.160 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HoareParallel
  32.161  
  32.162  
  32.163  ## HOL-MetisExamples
  32.164 @@ -510,7 +510,7 @@
  32.165    MetisExamples/BT.thy MetisExamples/Message.thy		\
  32.166    MetisExamples/Tarski.thy MetisExamples/TransClosure.thy	\
  32.167    MetisExamples/set.thy
  32.168 -	@$(ISATOOL) usedir $(OUT)/HOL MetisExamples
  32.169 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL MetisExamples
  32.170  
  32.171  
  32.172  ## HOL-Algebra
  32.173 @@ -533,7 +533,7 @@
  32.174    Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
  32.175    Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
  32.176    Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
  32.177 -	@cd Algebra; $(ISATOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
  32.178 +	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
  32.179  
  32.180  
  32.181  ## HOL-Auth
  32.182 @@ -557,7 +557,7 @@
  32.183    Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy		\
  32.184    Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy	\
  32.185    Auth/Smartcard/Smartcard.thy Auth/document/root.tex
  32.186 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
  32.187 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
  32.188  
  32.189  
  32.190  ## HOL-UNITY
  32.191 @@ -582,7 +582,7 @@
  32.192    UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy			\
  32.193    UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy			\
  32.194    UNITY/Comp/TimerArray.thy UNITY/document/root.tex
  32.195 -	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
  32.196 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
  32.197  
  32.198  
  32.199  ## HOL-Unix
  32.200 @@ -592,7 +592,7 @@
  32.201  $(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy	\
  32.202    Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy		\
  32.203    Unix/document/root.bib Unix/document/root.tex
  32.204 -	@$(ISATOOL) usedir $(OUT)/HOL Unix
  32.205 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
  32.206  
  32.207  
  32.208  ## HOL-ZF
  32.209 @@ -601,7 +601,7 @@
  32.210  
  32.211  $(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy	\
  32.212    ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
  32.213 -	@$(ISATOOL) usedir $(OUT)/HOL ZF
  32.214 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
  32.215  
  32.216  
  32.217  ## HOL-Modelcheck
  32.218 @@ -613,7 +613,7 @@
  32.219    Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy	\
  32.220    Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy		\
  32.221    Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
  32.222 -	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
  32.223 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck
  32.224  
  32.225  
  32.226  ## HOL-SizeChange
  32.227 @@ -626,7 +626,7 @@
  32.228    SizeChange/Interpretation.thy SizeChange/Implementation.thy		\
  32.229    SizeChange/Size_Change_Termination.thy SizeChange/Examples.thy	\
  32.230    SizeChange/sct.ML SizeChange/ROOT.ML
  32.231 -	@$(ISATOOL) usedir $(OUT)/HOL SizeChange
  32.232 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL SizeChange
  32.233  
  32.234  
  32.235  ## HOL-Lambda
  32.236 @@ -639,7 +639,7 @@
  32.237    Lambda/ParRed.thy Lambda/Standardization.thy Lambda/StrongNorm.thy	\
  32.238    Lambda/Type.thy Lambda/WeakNorm.thy Lambda/ROOT.ML			\
  32.239    Lambda/document/root.bib Lambda/document/root.tex
  32.240 -	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
  32.241 +	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
  32.242  
  32.243  
  32.244  ## HOL-Prolog
  32.245 @@ -648,7 +648,7 @@
  32.246  
  32.247  $(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML	\
  32.248    Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
  32.249 -	@$(ISATOOL) usedir $(OUT)/HOL Prolog
  32.250 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
  32.251  
  32.252  
  32.253  ## HOL-W0
  32.254 @@ -656,7 +656,7 @@
  32.255  HOL-W0: HOL $(LOG)/HOL-W0.gz
  32.256  
  32.257  $(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex
  32.258 -	@$(ISATOOL) usedir $(OUT)/HOL W0
  32.259 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL W0
  32.260  
  32.261  
  32.262  ## HOL-MicroJava
  32.263 @@ -692,7 +692,7 @@
  32.264    MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy			\
  32.265    MicroJava/document/root.bib MicroJava/document/root.tex		\
  32.266    MicroJava/document/introduction.tex
  32.267 -	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
  32.268 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
  32.269  
  32.270  
  32.271  ## HOL-NanoJava
  32.272 @@ -703,7 +703,7 @@
  32.273    NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy		\
  32.274    NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy		\
  32.275    NanoJava/document/root.bib NanoJava/document/root.tex
  32.276 -	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
  32.277 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
  32.278  
  32.279  
  32.280  ## HOL-Bali
  32.281 @@ -718,7 +718,7 @@
  32.282    Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
  32.283    Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
  32.284    Bali/WellType.thy Bali/document/root.tex
  32.285 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
  32.286 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
  32.287  
  32.288  
  32.289  ## HOL-Extraction
  32.290 @@ -731,7 +731,7 @@
  32.291    Extraction/QuotRem.thy Extraction/ROOT.ML Extraction/Util.thy	\
  32.292    Extraction/Warshall.thy Extraction/document/root.tex		\
  32.293    Extraction/document/root.bib
  32.294 -	@$(ISATOOL) usedir $(OUT)/HOL Extraction
  32.295 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Extraction
  32.296  
  32.297  
  32.298  ## HOL-IOA
  32.299 @@ -740,7 +740,7 @@
  32.300  
  32.301  $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
  32.302    IOA/Solve.thy
  32.303 -	@$(ISATOOL) usedir $(OUT)/HOL IOA
  32.304 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
  32.305  
  32.306  
  32.307  ## HOL-AxClasses
  32.308 @@ -749,7 +749,7 @@
  32.309  
  32.310  $(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
  32.311    AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
  32.312 -	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
  32.313 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
  32.314  
  32.315  
  32.316  ## HOL-Lattice
  32.317 @@ -759,7 +759,7 @@
  32.318  $(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
  32.319    Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy	\
  32.320    Lattice/ROOT.ML Lattice/document/root.tex
  32.321 -	@$(ISATOOL) usedir $(OUT)/HOL Lattice
  32.322 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
  32.323  
  32.324  
  32.325  ## HOL-ex
  32.326 @@ -796,7 +796,7 @@
  32.327    Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
  32.328    Complex/ex/ReflectedFerrack.thy					\
  32.329    Complex/ex/linrtac.ML
  32.330 -	@$(ISATOOL) usedir $(OUT)/HOL ex
  32.331 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
  32.332  
  32.333  
  32.334  ## HOL-Isar_examples
  32.335 @@ -814,7 +814,7 @@
  32.336    Isar_examples/ROOT.ML Isar_examples/document/proof.sty		\
  32.337    Isar_examples/document/root.bib Isar_examples/document/root.tex	\
  32.338    Isar_examples/document/style.tex Hoare/hoare_tac.ML
  32.339 -	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
  32.340 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_examples
  32.341  
  32.342  
  32.343  ## HOL-SET-Protocol
  32.344 @@ -826,7 +826,7 @@
  32.345    SET-Protocol/PublicSET.thy SET-Protocol/Cardholder_Registration.thy	\
  32.346    SET-Protocol/Merchant_Registration.thy SET-Protocol/Purchase.thy	\
  32.347    SET-Protocol/document/root.tex
  32.348 -	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
  32.349 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET-Protocol
  32.350  
  32.351  
  32.352  ## HOL-Matrix
  32.353 @@ -847,7 +847,7 @@
  32.354    Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\
  32.355    Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML	\
  32.356    Matrix/cplex/matrixlp.ML
  32.357 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
  32.358 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
  32.359  
  32.360  
  32.361  ## TLA
  32.362 @@ -856,7 +856,7 @@
  32.363  
  32.364  $(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy	\
  32.365    TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
  32.366 -	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
  32.367 +	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
  32.368  
  32.369  
  32.370  ## TLA-Inc
  32.371 @@ -864,7 +864,7 @@
  32.372  TLA-Inc: TLA $(LOG)/TLA-Inc.gz
  32.373  
  32.374  $(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
  32.375 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
  32.376 +	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
  32.377  
  32.378  
  32.379  ## TLA-Buffer
  32.380 @@ -872,7 +872,7 @@
  32.381  TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
  32.382  
  32.383  $(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
  32.384 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
  32.385 +	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
  32.386  
  32.387  
  32.388  ## TLA-Memory
  32.389 @@ -884,7 +884,7 @@
  32.390    TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy	\
  32.391    TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy			\
  32.392    TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
  32.393 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
  32.394 +	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
  32.395  
  32.396  
  32.397  ## HOL-Nominal
  32.398 @@ -902,7 +902,7 @@
  32.399    Nominal/nominal_primrec.ML \
  32.400    Nominal/nominal_thmdecls.ML \
  32.401    Library/Infinite_Set.thy
  32.402 -	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
  32.403 +	@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
  32.404  
  32.405  
  32.406  ## HOL-Nominal-Examples
  32.407 @@ -931,7 +931,7 @@
  32.408    Nominal/Examples/VC_Condition.thy \
  32.409    Nominal/Examples/W.thy \
  32.410    Nominal/Examples/Weakening.thy
  32.411 -	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
  32.412 +	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
  32.413  
  32.414  
  32.415  ## HOL-Word
  32.416 @@ -946,7 +946,7 @@
  32.417    Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
  32.418    Word/WordGenLib.thy Word/WordMain.thy Word/document/root.tex		\
  32.419    Word/document/root.bib
  32.420 -	@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
  32.421 +	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
  32.422  
  32.423  
  32.424  ## HOL-Word-Examples
  32.425 @@ -955,7 +955,7 @@
  32.426  
  32.427  $(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML	\
  32.428    Word/Examples/WordExamples.thy
  32.429 -	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
  32.430 +	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
  32.431  
  32.432  
  32.433  ## HOL-Statespace
  32.434 @@ -967,7 +967,7 @@
  32.435    Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy		\
  32.436    Statespace/distinct_tree_prover.ML Statespace/state_space.ML		\
  32.437    Statespace/state_fun.ML Statespace/document/root.tex
  32.438 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
  32.439 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
  32.440  
  32.441  
  32.442  ## HOL-NSA
  32.443 @@ -999,7 +999,7 @@
  32.444    Library/Infinite_Set.thy \
  32.445    Library/Zorn.thy \
  32.446    NSA/ROOT.ML
  32.447 -	@cd NSA; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
  32.448 +	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
  32.449  
  32.450  
  32.451  ## HOL-NSA-Examples
  32.452 @@ -1008,7 +1008,7 @@
  32.453  
  32.454  $(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML	\
  32.455    NSA/Examples/NSPrimes.thy
  32.456 -	@cd NSA; $(ISATOOL) usedir $(OUT)/HOL-NSA Examples
  32.457 +	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
  32.458  
  32.459  
  32.460  ## clean

    33.1 --- a/src/HOLCF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    33.2 +++ b/src/HOLCF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    33.3 @@ -25,7 +25,7 @@
    33.4  HOLCF: HOL $(OUT)/HOLCF
    33.5  
    33.6  HOL:
    33.7 -	@cd $(SRC)/HOL; $(ISATOOL) make HOL
    33.8 +	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
    33.9  
   33.10  $(OUT)/HOLCF: $(OUT)/HOL \
   33.11    ROOT.ML \
   33.12 @@ -71,7 +71,7 @@
   33.13    Tools/pcpodef_package.ML \
   33.14    holcf_logic.ML \
   33.15    document/root.tex
   33.16 -	@$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
   33.17 +	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
   33.18  
   33.19  
   33.20  ## HOLCF-IMP
   33.21 @@ -80,7 +80,7 @@
   33.22  
   33.23  $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
   33.24    IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
   33.25 -	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
   33.26 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
   33.27  
   33.28  
   33.29  ## HOLCF-ex
   33.30 @@ -90,7 +90,7 @@
   33.31  $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \
   33.32    ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \
   33.33    ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy
   33.34 -	@$(ISATOOL) usedir $(OUT)/HOLCF ex
   33.35 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
   33.36  
   33.37  
   33.38  ## HOLCF-FOCUS
   33.39 @@ -101,7 +101,7 @@
   33.40    FOCUS/Fstream.thy FOCUS/FOCUS.thy \
   33.41    FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
   33.42    FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
   33.43 -	@$(ISATOOL) usedir $(OUT)/HOLCF FOCUS
   33.44 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
   33.45  
   33.46  ## IOA
   33.47  
   33.48 @@ -118,7 +118,7 @@
   33.49    IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \
   33.50    IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \
   33.51    IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
   33.52 -	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
   33.53 +	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
   33.54  
   33.55  
   33.56  ## IOA-ABP
   33.57 @@ -132,7 +132,7 @@
   33.58    IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
   33.59    IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
   33.60    IOA/ABP/Spec.thy
   33.61 -	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
   33.62 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
   33.63  
   33.64  ## IOA-NTP
   33.65  
   33.66 @@ -143,7 +143,7 @@
   33.67    IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \
   33.68    IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \
   33.69    IOA/NTP/Spec.thy
   33.70 -	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
   33.71 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
   33.72  
   33.73  
   33.74  ## IOA-Modelcheck
   33.75 @@ -153,7 +153,7 @@
   33.76  $(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \
   33.77    IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \
   33.78    IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy
   33.79 -	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck
   33.80 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck
   33.81  
   33.82  
   33.83  ## IOA-Storage
   33.84 @@ -163,7 +163,7 @@
   33.85  $(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \
   33.86    IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
   33.87    IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
   33.88 -	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage
   33.89 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
   33.90  
   33.91  
   33.92  ## IOA-ex
   33.93 @@ -171,7 +171,7 @@
   33.94  IOA-ex: IOA $(LOG)/IOA-ex.gz
   33.95  
   33.96  $(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy
   33.97 -	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ex
   33.98 +	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
   33.99  
  33.100  
  33.101  ## clean

    34.1 --- a/src/LCF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    34.2 +++ b/src/LCF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    34.3 @@ -24,10 +24,10 @@
    34.4  LCF: FOL $(OUT)/LCF
    34.5  
    34.6  FOL:
    34.7 -	@cd $(SRC)/FOL; $(ISATOOL) make FOL
    34.8 +	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
    34.9  
   34.10  $(OUT)/LCF: $(OUT)/FOL LCF.thy ROOT.ML
   34.11 -	@$(ISATOOL) usedir -b -r $(OUT)/FOL LCF
   34.12 +	@$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL LCF
   34.13  
   34.14  
   34.15  ## LCF-ex
   34.16 @@ -35,7 +35,7 @@
   34.17  LCF-ex: LCF $(LOG)/LCF-ex.gz
   34.18  
   34.19  $(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.thy ex/Ex2.thy ex/Ex3.thy ex/Ex4.thy ex/ROOT.ML
   34.20 -	@$(ISATOOL) usedir $(OUT)/LCF ex
   34.21 +	@$(ISABELLE_TOOL) usedir $(OUT)/LCF ex
   34.22  
   34.23  
   34.24  ## clean

    35.1 --- a/src/Pure/General/file.ML	Sat Oct 04 16:05:08 2008 +0200
    35.2 +++ b/src/Pure/General/file.ML	Sat Oct 04 16:05:09 2008 +0200
    35.3 @@ -66,7 +66,7 @@
    35.4  
    35.5  (* system commands *)
    35.6  
    35.7 -fun isabelle_tool cmd = system ("\"$ISATOOL\" " ^ cmd);
    35.8 +fun isabelle_tool cmd = system ("\"$ISABELLE_TOOL\" " ^ cmd);
    35.9  
   35.10  fun system_command cmd =
   35.11    if system cmd <> 0 then error ("System command failed: " ^ cmd)

    36.1 --- a/src/Pure/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    36.2 +++ b/src/Pure/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    36.3 @@ -92,7 +92,7 @@
    36.4  Pure-ProofGeneral: Pure $(LOG)/Pure-ProofGeneral.gz
    36.5  
    36.6  $(LOG)/Pure-ProofGeneral.gz: $(OUT)/Pure ProofGeneral/proof_general_keywords.ML
    36.7 -	@$(ISATOOL) usedir -f proof_general_keywords.ML $(OUT)/Pure ProofGeneral
    36.8 +	@$(ISABELLE_TOOL) usedir -f proof_general_keywords.ML $(OUT)/Pure ProofGeneral
    36.9  
   36.10  
   36.11  RAW: $(OUT)/RAW

    37.1 --- a/src/Pure/Thy/present.ML	Sat Oct 04 16:05:08 2008 +0200
    37.2 +++ b/src/Pure/Thy/present.ML	Sat Oct 04 16:05:09 2008 +0200
    37.3 @@ -325,7 +325,7 @@
    37.4  
    37.5  fun isabelle_document verbose format name tags path result_path =
    37.6    let
    37.7 -    val s = "\"$ISATOOL\" document -c -o '" ^ format ^ "' \
    37.8 +    val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
    37.9        \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
   37.10        " 2>&1" ^ (if verbose then "" else " >/dev/null");
   37.11      val doc_path = Path.append result_path (Path.ext format (Path.basic name));

    38.1 --- a/src/Pure/Tools/isabelle_system.scala	Sat Oct 04 16:05:08 2008 +0200
    38.2 +++ b/src/Pure/Tools/isabelle_system.scala	Sat Oct 04 16:05:09 2008 +0200
    38.3 @@ -93,7 +93,7 @@
    38.4  
    38.5    def isabelle_tool(args: String*) = {
    38.6      val proc =
    38.7 -      try { exec2((List(getenv_strict("ISATOOL")) ++ args): _*) }
    38.8 +      try { exec2((List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
    38.9        catch { case e: IOException => error(e.getMessage) }
   38.10      proc.getOutputStream.close
   38.11      val output = Source.fromInputStream(proc.getInputStream, charset).mkString("")

    39.1 --- a/src/Sequents/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    39.2 +++ b/src/Sequents/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    39.3 @@ -24,12 +24,12 @@
    39.4  Sequents: Pure $(OUT)/Sequents
    39.5  
    39.6  Pure:
    39.7 -	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    39.8 +	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    39.9  
   39.10  $(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \
   39.11    modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
   39.12    ILL_predlog.thy Washing.thy
   39.13 -	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
   39.14 +	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure Sequents
   39.15  
   39.16  
   39.17  ## Sequents-LK
   39.18 @@ -38,7 +38,7 @@
   39.19  
   39.20  $(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/Hard_Quantifiers.thy \
   39.21    LK/Propositional.thy LK/Quantifiers.thy LK/Nat.thy
   39.22 -	@$(ISATOOL) usedir $(OUT)/Sequents LK
   39.23 +	@$(ISABELLE_TOOL) usedir $(OUT)/Sequents LK
   39.24  
   39.25  
   39.26  ## clean

    40.1 --- a/src/ZF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
    40.2 +++ b/src/ZF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
    40.3 @@ -26,7 +26,7 @@
    40.4  ZF: FOL $(OUT)/ZF
    40.5  
    40.6  FOL:
    40.7 -	@cd $(SRC)/FOL; $(ISATOOL) make FOL
    40.8 +	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
    40.9  
   40.10  $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy	\
   40.11    Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy	\
   40.12 @@ -40,7 +40,7 @@
   40.13    Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy	\
   40.14    ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML	\
   40.15    int_arith.ML pair.thy simpdata.ML upair.thy
   40.16 -	@$(ISATOOL) usedir -b -g true -r $(OUT)/FOL ZF
   40.17 +	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF
   40.18  
   40.19  
   40.20  ## ZF-AC
   40.21 @@ -52,7 +52,7 @@
   40.22    AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy		\
   40.23    AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy		\
   40.24    AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
   40.25 -	@$(ISATOOL) usedir -g true $(OUT)/ZF AC
   40.26 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF AC
   40.27  
   40.28  
   40.29  ## ZF-Coind
   40.30 @@ -62,7 +62,7 @@
   40.31  $(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy		\
   40.32    Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy	\
   40.33    Coind/Types.thy Coind/Values.thy
   40.34 -	@$(ISATOOL) usedir $(OUT)/ZF Coind
   40.35 +	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Coind
   40.36  
   40.37  
   40.38  ## ZF-Constructible
   40.39 @@ -80,7 +80,7 @@
   40.40    Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy	\
   40.41    Constructible/Reflection.thy Constructible/WFrec.thy			\
   40.42    Constructible/document/root.bib Constructible/document/root.tex
   40.43 -	@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible
   40.44 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF Constructible
   40.45  
   40.46  
   40.47  ## ZF-IMP
   40.48 @@ -90,7 +90,7 @@
   40.49  $(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy	\
   40.50    IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib		\
   40.51    IMP/document/root.tex
   40.52 -	@$(ISATOOL) usedir $(OUT)/ZF IMP
   40.53 +	@$(ISABELLE_TOOL) usedir $(OUT)/ZF IMP
   40.54  
   40.55  
   40.56  ## ZF-Resid
   40.57 @@ -100,7 +100,7 @@
   40.58  $(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy	\
   40.59    Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy		\
   40.60    Resid/Substitution.thy
   40.61 -	@$(ISATOOL) usedir $(OUT)/ZF Resid
   40.62 +	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Resid
   40.63  
   40.64  
   40.65  ## ZF-UNITY
   40.66 @@ -114,7 +114,7 @@
   40.67    UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy		\
   40.68    UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy		\
   40.69    UNITY/MultisetSum.thy UNITY/WFair.thy
   40.70 -	@$(ISATOOL) usedir $(OUT)/ZF UNITY
   40.71 +	@$(ISABELLE_TOOL) usedir $(OUT)/ZF UNITY
   40.72  
   40.73  
   40.74  ## ZF-Induct
   40.75 @@ -127,7 +127,7 @@
   40.76    Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy			\
   40.77    Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy			\
   40.78    Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
   40.79 -	@$(ISATOOL) usedir $(OUT)/ZF Induct
   40.80 +	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Induct
   40.81  
   40.82  
   40.83  ## ZF-ex
   40.84 @@ -137,7 +137,7 @@
   40.85  $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy	\
   40.86    ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy		\
   40.87    ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy
   40.88 -	@$(ISATOOL) usedir $(OUT)/ZF ex
   40.89 +	@$(ISABELLE_TOOL) usedir $(OUT)/ZF ex
   40.90  
   40.91  
   40.92  ## clean