# HG changeset patch
# User wenzelm
# Date 1117528760 -7200
# Node ID ae921f717a2b64fd456994198722a4d5944489a9
# Parent  8d453f906e43a502b57383bbcf9e1b9fdc3b1ad1
tuned;

diff -r 8d453f906e43 -r ae921f717a2b src/Pure/README
--- a/src/Pure/README	Mon May 30 23:07:58 2005 +0200
+++ b/src/Pure/README	Tue May 31 10:39:20 2005 +0200
@@ -3,15 +3,19 @@
 
 
 This directory contains the ML source files for Pure Isabelle, which
-is the basis for all object-logics:
+is the basis for all object-logics.  The Isabelle/Pure image may be
+compiled in batch mode like this:
+
+  isatool make Pure
+
+Developers may want to produce a RAW image that merely consists of the
+ML compiler with the compatibility setup of ML-Systems/ preloaded:
 
-  IsaMakefile	compiles the Pure system (use isatool make)
-  ML-Systems/   compatibility files for various ML systems
-  General/	general tools
-  Syntax/     	the syntax module
-  Thy/          the theory file parser (old format) and loader
-  Isar/		Intelligible Semi-Automated Reasoning subsystem
-  ./		the actual meta logic implementation (see ROOT.ML)
+  isatool make RAW
+
+Now the Pure session may be compiled interactively as follows:
 
-Isabelle programmers may want to have a look at the generic modules
-Library (see library.ML) and those in General/ (see General/README).
+  isabelle -u RAW
+
+
+$Id$