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