--- 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$