isabelle: src/HOL/Import/HOL4/README@880e587eee9f (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
46800 9696218b02fe avoid internal hol4 name references in generic importer code haftmann parents: 46799 diff changeset	5	All the files in this directory (except this README, Importer.thy, and
14516 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	Cezary Kaliszyk <cezarykaliszyk@gmail.com>
	Sun, 01 Apr 2012 14:50:47 +0200
changeset 47258	880e587eee9f
parent 46800	src/HOL/Import/README@9696218b02fe
permissions	-rw-r--r--