Mercurial Mercurial > repos > isabelle / comparison
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/HOL4/README
changeset 47258 880e587eee9f
parent 46800 9696218b02fe
equal deleted inserted replaced
47244:a7f85074c169 47258:880e587eee9f 
       
     1 
       
     2 ATTENTION!  This is largely outdated.  The hint to PROOF_DIRS might be
 
       
     3 everything which is still relevant.
 
       
     4 
       
     5 All the files in this directory (except this README, Importer.thy, and
 
       
     6 ROOT.ML) are automatically generated.  Edit the files in
 
       
     7 ../Generate-HOL and run "isabelle make HOL-Complex-Generate-HOL" in
 
       
     8 ~~/src/HOL, if something needs to be changed.
 
       
     9 
       
    10 To build the logic in this directory, simply do a "isabelle make
 
       
    11 HOL-Import-HOL" in ~~/src/HOL.
 
       
    12 
       
    13 Note that the quick_and_dirty flag is on as default for this
 
       
    14 directory, which means that the original external proofs are not consulted
 
       
    15 at all.  If a real replay of the external proofs is desired, get and
 
       
    16 unpack the external proof objects to somewhere on your harddisk, and set
 
       
    17 the variable PROOF_DIRS to the directory where the directory "hol4"
 
       
    18 is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
 
       
    19 do "isabelle make HOL-Import-HOL" in ~~/src/HOL.
isabelle