Tue, 31 May 2005 10:39:20 +0200
changeset 16115 ae921f717a2b
parent 16114 8d453f906e43
child 16116 bb7ba5c5e632
--- 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