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;
     1 
     2                         Pure: The Pure Isabelle System
     3 
     4 
     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:
     8 
     9   $ isabelle build Pure
    10 
    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
    15 
    16 or alternatively the raw Poly/ML console:
    17 
    18   $ isabelle console -r
    19   Poly/ML> use "ROOT0.ML";
    20   Poly/ML> use "ROOT.ML";