--- a/src/HOL/Import/HOL/README Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/README Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,20 @@
+(* Title: HOL/Import/HOL/README
+ ID: $Id$
+ Author: Sebastian Skalberg (TU Muenchen)
+*)
+
All the files in this directory (except this README, HOL4.thy, and
ROOT.ML) are automatically generated. Edit the files in
-../Generate-HOL, if something needs to be changed.
+../Generate-HOL and run "isatool 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
+HOL-Import-HOL" in ~~/src/HOL.
+
+Note that the quick_and_dirty flag is on as default for this
+directory, which means that the original HOL4 proofs are not consulted
+at all. If a real replay of the HOL4 proofs is desired, get and
+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.