| 
4689
 | 
     1  | 
  | 
| 
19
 | 
     2  | 
                        Pure: The Pure Isabelle System
  | 
| 
0
 | 
     3  | 
  | 
| 
4689
 | 
     4  | 
  | 
| 
67102
 | 
     5  | 
This directory contains the ML source files for Pure Isabelle, which is
  | 
| 
 | 
     6  | 
the basis for all object-logics. Building the Isabelle/Pure heap image
  | 
| 
 | 
     7  | 
in batch mode works as follows:
  | 
| 
16115
 | 
     8  | 
  | 
| 
67102
 | 
     9  | 
  $ isabelle build Pure
  | 
| 
16115
 | 
    10  | 
  | 
| 
67102
 | 
    11  | 
To explore the bootstrap of Pure interactively, the Prover IDE can be
  | 
| 
 | 
    12  | 
used like this:
  | 
| 
 | 
    13  | 
  | 
| 
 | 
    14  | 
  $ isabelle jedit -l Pure ROOT.ML
  | 
| 
0
 | 
    15  | 
  | 
| 
67102
 | 
    16  | 
or alternatively the raw Poly/ML console:
  | 
| 
16115
 | 
    17  | 
  | 
| 
67102
 | 
    18  | 
  $ isabelle console -r
  | 
| 
 | 
    19  | 
  Poly/ML> use "ROOT0.ML";
  | 
| 
 | 
    20  | 
  Poly/ML> use "ROOT.ML";
  |