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