author  wenzelm 
Sat, 04 Oct 2008 17:40:56 +0200  
changeset 28504  7ad7d7d6df47 
parent 14620  1be590fd2422 
permissions  rwrr 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

1 
(* Title: HOL/Import/HOL/README 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

2 
ID: $Id$ 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

3 
Author: Sebastian Skalberg (TU Muenchen) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

4 
*) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

5 

14516  6 
All the files in this directory (except this README, HOL4.thy, and 
7 
ROOT.ML) are automatically generated. Edit the files in 

28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelleprocess), renamed isatool to isabelle;
wenzelm
parents:
14620
diff
changeset

8 
../GenerateHOL and run "isabelle make HOLComplexGenerateHOL" in 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

9 
~~/src/HOL, if something needs to be changed. 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

10 

28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelleprocess), renamed isatool to isabelle;
wenzelm
parents:
14620
diff
changeset

11 
To build the logic in this directory, simply do a "isabelle make 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

12 
HOLImportHOL" in ~~/src/HOL. 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

13 

1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

14 
Note that the quick_and_dirty flag is on as default for this 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

15 
directory, which means that the original HOL4 proofs are not consulted 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

16 
at all. If a real replay of the HOL4 proofs is desired, get and 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

17 
unpack the HOL4 proof objects to somewhere on your harddisk, and set 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

18 
the variable PROOF_DIRS to the directory where the directory "hol4" 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset

19 
is. Now edit the ROOT.ML file to unset the quick_and_dirty flag and 
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelleprocess), renamed isatool to isabelle;
wenzelm
parents:
14620
diff
changeset

20 
do "isabelle make HOLImportHOL" in ~~/src/HOL. 