tuned;
authorwenzelm
Tue May 31 10:39:20 2005 +0200 (2005-05-31)
changeset 16115ae921f717a2b
parent 16114 8d453f906e43
child 16116 bb7ba5c5e632
tuned;
src/Pure/README
     1.1 --- a/src/Pure/README	Mon May 30 23:07:58 2005 +0200
     1.2 +++ b/src/Pure/README	Tue May 31 10:39:20 2005 +0200
     1.3 @@ -3,15 +3,19 @@
     1.4  
     1.5  
     1.6  This directory contains the ML source files for Pure Isabelle, which
     1.7 -is the basis for all object-logics:
     1.8 +is the basis for all object-logics.  The Isabelle/Pure image may be
     1.9 +compiled in batch mode like this:
    1.10 +
    1.11 +  isatool make Pure
    1.12 +
    1.13 +Developers may want to produce a RAW image that merely consists of the
    1.14 +ML compiler with the compatibility setup of ML-Systems/ preloaded:
    1.15  
    1.16 -  IsaMakefile	compiles the Pure system (use isatool make)
    1.17 -  ML-Systems/   compatibility files for various ML systems
    1.18 -  General/	general tools
    1.19 -  Syntax/     	the syntax module
    1.20 -  Thy/          the theory file parser (old format) and loader
    1.21 -  Isar/		Intelligible Semi-Automated Reasoning subsystem
    1.22 -  ./		the actual meta logic implementation (see ROOT.ML)
    1.23 +  isatool make RAW
    1.24 +
    1.25 +Now the Pure session may be compiled interactively as follows:
    1.26  
    1.27 -Isabelle programmers may want to have a look at the generic modules
    1.28 -Library (see library.ML) and those in General/ (see General/README).
    1.29 +  isabelle -u RAW
    1.30 +
    1.31 +
    1.32 +$Id$