src/HOL/Import/HOL/README
author skalberg
Sat Apr 17 23:53:35 2004 +0200 (2004-04-17)
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 28504 7ad7d7d6df47
permissions -rw-r--r--
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg@14620
     1
(*  Title:      HOL/Import/HOL/README
skalberg@14620
     2
    ID:         $Id$
skalberg@14620
     3
    Author:     Sebastian Skalberg (TU Muenchen)
skalberg@14620
     4
*)
skalberg@14620
     5
skalberg@14516
     6
All the files in this directory (except this README, HOL4.thy, and
skalberg@14516
     7
ROOT.ML) are automatically generated.  Edit the files in
skalberg@14620
     8
../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in
skalberg@14620
     9
~~/src/HOL, if something needs to be changed.
skalberg@14620
    10
skalberg@14620
    11
To build the logic in this directory, simply do a "isatool make
skalberg@14620
    12
HOL-Import-HOL" in ~~/src/HOL.
skalberg@14620
    13
skalberg@14620
    14
Note that the quick_and_dirty flag is on as default for this
skalberg@14620
    15
directory, which means that the original HOL4 proofs are not consulted
skalberg@14620
    16
at all.  If a real replay of the HOL4 proofs is desired, get and
skalberg@14620
    17
unpack the HOL4 proof objects to somewhere on your harddisk, and set
skalberg@14620
    18
the variable PROOF_DIRS to the directory where the directory "hol4"
skalberg@14620
    19
is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
skalberg@14620
    20
do "isatool make HOL-Import-HOL" in ~~/src/HOL.