Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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;

(*  Title:      HOL/Import/HOL/README
    ID:         $Id$
    Author:     Sebastian Skalberg (TU Muenchen)
*)

All the files in this directory (except this README, HOL4.thy, and
ROOT.ML) are automatically generated.  Edit the files in
../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" in
~~/src/HOL, if something needs to be changed.

To build the logic in this directory, simply do a "isabelle make
HOL-Import-HOL" in ~~/src/HOL.

Note that the quick_and_dirty flag is on as default for this
directory, which means that the original HOL4 proofs are not consulted
at all.  If a real replay of the HOL4 proofs is desired, get and
unpack the HOL4 proof objects to somewhere on your harddisk, and set
the variable PROOF_DIRS to the directory where the directory "hol4"
is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
do "isabelle make HOL-Import-HOL" in ~~/src/HOL.
isabelle