src/Pure/README
changeset 4689 49d116fdcafa
parent 4620 bfd40126c56e
child 4941 ac5da3e767b0
--- a/src/Pure/README	Mon Mar 09 16:06:46 1998 +0100
+++ b/src/Pure/README	Mon Mar 09 16:07:03 1998 +0100
@@ -1,12 +1,15 @@
+
                         Pure: The Pure Isabelle System
 
+
 This directory contains the ML source files for Pure Isabelle, which
 is the basis for all object-logics:
 
-  IsaMakefile	compiles the Pure system
+  IsaMakefile	compiles the Pure system (use isatool make)
   ML-Systems/   compatibility files for various ML systems
   Syntax/     	the syntax module
   Thy/          the theory file parser and loader
+  ./		the actual meta logic implementation (see ROOT.ML)
 
 Isabelle programmers may want to have a look at the following generic
 modules:
@@ -15,6 +18,8 @@
   TableFun	efficient tables (see table.ML)
   Seq		unbounded sequences (see seq.ML)
   Pretty	pretty printing module (see Syntax/pretty.ML)
-  Scanner	scanner toolbox (see Syntax/lexicon.ML)
+  Scan		scanner toolbox (see Syntax/scan.ML)
+  Symbol	baroque characters (see Syntax/symbol.ML)
   Path		abstract algebra of file paths (see Thy/path.ML)
   File		file system operations (see Thy/file.ML)
+  NameSpace	hierarchically structured name spaces (see name_space.ML)