src/HOL/Import/HOL/README
author wenzelm
Sat, 04 Oct 2008 17:40:56 +0200
changeset 28504 7ad7d7d6df47
parent 14620 1be590fd2422
permissions -rw-r--r--
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
All the files in this directory (except this README, HOL4.thy, and
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     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.