author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14620 1be590fd2422
child 28504 7ad7d7d6df47
permissions -rw-r--r--
adaptions to codegen_package
     1 (*  Title:      HOL/Import/HOL/README
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     6 All the files in this directory (except this README, HOL4.thy, and
     7 ROOT.ML) are automatically generated.  Edit the files in
     8 ../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in
     9 ~~/src/HOL, if something needs to be changed.
    11 To build the logic in this directory, simply do a "isatool make
    12 HOL-Import-HOL" in ~~/src/HOL.
    14 Note that the quick_and_dirty flag is on as default for this
    15 directory, which means that the original HOL4 proofs are not consulted
    16 at all.  If a real replay of the HOL4 proofs is desired, get and
    17 unpack the HOL4 proof objects to somewhere on your harddisk, and set
    18 the variable PROOF_DIRS to the directory where the directory "hol4"
    19 is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
    20 do "isatool make HOL-Import-HOL" in ~~/src/HOL.