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