isabelle: src/HOL/Import/HOL/README@9dba9c7872c9 (annotated)

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
14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	8	../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in
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
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	11	To build the logic in this directory, simply do a "isatool make
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
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	20	do "isatool make HOL-Import-HOL" in ~~/src/HOL.

author	haftmann
	Tue, 19 Sep 2006 15:22:35 +0200
changeset 20604	9dba9c7872c9
parent 14620	1be590fd2422
child 28504	7ad7d7d6df47
permissions	-rw-r--r--