# HG changeset patch
# User wenzelm
# Date 889456023 -3600
# Node ID 49d116fdcafac802f92e4579e78133d5de99f5ce
# Parent  033566671199c568024f43179558a7e9a6d6b5aa
tuned;

diff -r 033566671199 -r 49d116fdcafa src/Pure/README
--- 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)
diff -r 033566671199 -r 49d116fdcafa src/Pure/Syntax/README
--- a/src/Pure/Syntax/README	Mon Mar 09 16:06:46 1998 +0100
+++ b/src/Pure/Syntax/README	Mon Mar 09 16:07:03 1998 +0100
@@ -1,14 +1,14 @@
+
                               Pure/Syntax/
 
-This directory contains the source files for Isabelle's syntax module, which
-includes a lexer, parser, pretty printer and macro system. Note that only the
-following structures are supposed to be exported:
+
+This directory contains the source files for Isabelle's syntax module,
+which includes a lexer, parser, pretty printer and macro system. Note
+that only the following structures are supposed to be exported:
 
   Pretty        (generic pretty printing module)
-  Scanner       (generic scanner toolbox)
+  Scan          (generic scanner toolbox)
+  Symbol	(baroque characters)
 
   Syntax        (internal interface to the syntax module)
   BasicSyntax   (part of Syntax made pervasive)
-
-There is no IsaMakefile to compile these files separately; they are
-compiled as part of Pure Isabelle.