| author | haftmann |
| Thu, 29 Apr 2010 15:00:41 +0200 | |
| changeset 36533 | f8df589ca2a5 |
| parent 28504 | 7ad7d7d6df47 |
| permissions | -rw-r--r-- |
|
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 isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
14620
diff
changeset
|
8 |
../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" 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 isabelle-process), 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 |
HOL-Import-HOL" 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 isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
14620
diff
changeset
|
20 |
do "isabelle make HOL-Import-HOL" in ~~/src/HOL. |