updated documentation;
authorwenzelm
Mon Nov 27 16:48:55 2017 +0100 (7 months ago)
changeset 67102411e49edd905
parent 67101 60126738b2d0
child 67103 39cc38a06610
updated documentation;
src/Pure/README
     1.1 --- a/src/Pure/README	Mon Nov 27 16:44:32 2017 +0100
     1.2 +++ b/src/Pure/README	Mon Nov 27 16:48:55 2017 +0100
     1.3 @@ -2,15 +2,19 @@
     1.4                          Pure: The Pure Isabelle System
     1.5  
     1.6  
     1.7 -This directory contains the ML source files for Pure Isabelle, which
     1.8 -is the basis for all object-logics.  Building the Isabelle/Pure heap
     1.9 -image in batch mode works as for any other session:
    1.10 +This directory contains the ML source files for Pure Isabelle, which is
    1.11 +the basis for all object-logics. Building the Isabelle/Pure heap image
    1.12 +in batch mode works as follows:
    1.13  
    1.14 -  isabelle build -b Pure
    1.15 +  $ isabelle build Pure
    1.16  
    1.17 -To explore the bootstrap of Pure interactively, the raw ML console can
    1.18 -be used like this:
    1.19 +To explore the bootstrap of Pure interactively, the Prover IDE can be
    1.20 +used like this:
    1.21  
    1.22 -  isabelle console -l RAW
    1.23 -  use "ROOT.ML";
    1.24 +  $ isabelle jedit -l Pure ROOT.ML
    1.25  
    1.26 +or alternatively the raw Poly/ML console:
    1.27 +
    1.28 +  $ isabelle console -r
    1.29 +  Poly/ML> use "ROOT0.ML";
    1.30 +  Poly/ML> use "ROOT.ML";