isabelle: src/HOL/Import/README@f21494dc0bf6 (annotated)

46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 28504 diff changeset	1
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 28504 diff changeset	2	ATTENTION! This is largely outdated. The hint to PROOF_DIRS might be
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 28504 diff changeset	3	everything which is still relevant.
14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	4
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	5	All the files in this directory (except this README, HOL4.thy, and
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6	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	7	../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	8	~~/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	9
28504 7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle; wenzelm parents: 14620 diff changeset	10	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	11	HOL-Import-HOL" in ~~/src/HOL.
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	12
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	13	Note that the quick_and_dirty flag is on as default for this
46799 f21494dc0bf6 generalized user-visible text haftmann parents: 46787 diff changeset	14	directory, which means that the original external proofs are not consulted
f21494dc0bf6 generalized user-visible text haftmann parents: 46787 diff changeset	15	at all. If a real replay of the external proofs is desired, get and
f21494dc0bf6 generalized user-visible text haftmann parents: 46787 diff changeset	16	unpack the external proof objects to somewhere on your harddisk, and set
14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	17	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	18	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	19	do "isabelle make HOL-Import-HOL" in ~~/src/HOL.

author	haftmann
	Sat, 03 Mar 2012 23:54:44 +0100
changeset 46799	f21494dc0bf6
parent 46787	3d3d8f8929a7
child 46800	9696218b02fe
permissions	-rw-r--r--