3 Author: Sebastian Skalberg (TU Muenchen) |
3 Author: Sebastian Skalberg (TU Muenchen) |
4 *) |
4 *) |
5 |
5 |
6 All the files in this directory (except this README, HOL4.thy, and |
6 All the files in this directory (except this README, HOL4.thy, and |
7 ROOT.ML) are automatically generated. Edit the files in |
7 ROOT.ML) are automatically generated. Edit the files in |
8 ../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in |
8 ../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" in |
9 ~~/src/HOL, if something needs to be changed. |
9 ~~/src/HOL, if something needs to be changed. |
10 |
10 |
11 To build the logic in this directory, simply do a "isatool make |
11 To build the logic in this directory, simply do a "isabelle make |
12 HOL-Import-HOL" in ~~/src/HOL. |
12 HOL-Import-HOL" in ~~/src/HOL. |
13 |
13 |
14 Note that the quick_and_dirty flag is on as default for this |
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 |
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 |
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 |
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" |
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 |
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. |
20 do "isabelle make HOL-Import-HOL" in ~~/src/HOL. |