src/Pure/README
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 67102 411e49edd905
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
wenzelm@4689
     1
wenzelm@19
     2
                        Pure: The Pure Isabelle System
clasohm@0
     3
wenzelm@4689
     4
wenzelm@67102
     5
This directory contains the ML source files for Pure Isabelle, which is
wenzelm@67102
     6
the basis for all object-logics. Building the Isabelle/Pure heap image
wenzelm@67102
     7
in batch mode works as follows:
wenzelm@16115
     8
wenzelm@67102
     9
  $ isabelle build Pure
wenzelm@16115
    10
wenzelm@67102
    11
To explore the bootstrap of Pure interactively, the Prover IDE can be
wenzelm@67102
    12
used like this:
wenzelm@67102
    13
wenzelm@67102
    14
  $ isabelle jedit -l Pure ROOT.ML
clasohm@0
    15
wenzelm@67102
    16
or alternatively the raw Poly/ML console:
wenzelm@16115
    17
wenzelm@67102
    18
  $ isabelle console -r
wenzelm@67102
    19
  Poly/ML> use "ROOT0.ML";
wenzelm@67102
    20
  Poly/ML> use "ROOT.ML";