equal
deleted
inserted
replaced
1 |
|
2 ATTENTION! This is largely outdated. The hint to PROOF_DIRS might be |
|
3 everything which is still relevant. |
|
4 |
|
5 All the files in this directory (except this README, Importer.thy, and |
|
6 ROOT.ML) are automatically generated. Edit the files in |
|
7 ../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" in |
|
8 ~~/src/HOL, if something needs to be changed. |
|
9 |
|
10 To build the logic in this directory, simply do a "isabelle make |
|
11 HOL-Import-HOL" in ~~/src/HOL. |
|
12 |
|
13 Note that the quick_and_dirty flag is on as default for this |
|
14 directory, which means that the original external proofs are not consulted |
|
15 at all. If a real replay of the external proofs is desired, get and |
|
16 unpack the external proof objects to somewhere on your harddisk, and set |
|
17 the variable PROOF_DIRS to the directory where the directory "hol4" |
|
18 is. Now edit the ROOT.ML file to unset the quick_and_dirty flag and |
|
19 do "isabelle make HOL-Import-HOL" in ~~/src/HOL. |
|