tuned;
authorwenzelm
Mon Mar 09 16:07:03 1998 +0100 (1998-03-09)
changeset 468949d116fdcafa
parent 4688 033566671199
child 4690 8459cf322011
tuned;
src/Pure/README
src/Pure/Syntax/README
     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)
     2.1 --- a/src/Pure/Syntax/README	Mon Mar 09 16:06:46 1998 +0100
     2.2 +++ b/src/Pure/Syntax/README	Mon Mar 09 16:07:03 1998 +0100
     2.3 @@ -1,14 +1,14 @@
     2.4 +
     2.5                                Pure/Syntax/
     2.6  
     2.7 -This directory contains the source files for Isabelle's syntax module, which
     2.8 -includes a lexer, parser, pretty printer and macro system. Note that only the
     2.9 -following structures are supposed to be exported:
    2.10 +
    2.11 +This directory contains the source files for Isabelle's syntax module,
    2.12 +which includes a lexer, parser, pretty printer and macro system. Note
    2.13 +that only the following structures are supposed to be exported:
    2.14  
    2.15    Pretty        (generic pretty printing module)
    2.16 -  Scanner       (generic scanner toolbox)
    2.17 +  Scan          (generic scanner toolbox)
    2.18 +  Symbol	(baroque characters)
    2.19  
    2.20    Syntax        (internal interface to the syntax module)
    2.21    BasicSyntax   (part of Syntax made pervasive)
    2.22 -
    2.23 -There is no IsaMakefile to compile these files separately; they are
    2.24 -compiled as part of Pure Isabelle.