src/HOL/Import/HOL/README
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 28504 7ad7d7d6df47
     1.1 --- a/src/HOL/Import/HOL/README	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/HOL/README	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,3 +1,20 @@
     1.4 +(*  Title:      HOL/Import/HOL/README
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9  All the files in this directory (except this README, HOL4.thy, and
    1.10  ROOT.ML) are automatically generated.  Edit the files in
    1.11 -../Generate-HOL, if something needs to be changed.
    1.12 +../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in
    1.13 +~~/src/HOL, if something needs to be changed.
    1.14 +
    1.15 +To build the logic in this directory, simply do a "isatool make
    1.16 +HOL-Import-HOL" in ~~/src/HOL.
    1.17 +
    1.18 +Note that the quick_and_dirty flag is on as default for this
    1.19 +directory, which means that the original HOL4 proofs are not consulted
    1.20 +at all.  If a real replay of the HOL4 proofs is desired, get and
    1.21 +unpack the HOL4 proof objects to somewhere on your harddisk, and set
    1.22 +the variable PROOF_DIRS to the directory where the directory "hol4"
    1.23 +is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
    1.24 +do "isatool make HOL-Import-HOL" in ~~/src/HOL.