src/Pure/README
author wenzelm
Sun, 19 May 2024 18:43:45 +0200
changeset 80181 aa92c0f96036
parent 67102 411e49edd905
permissions -rw-r--r--
provide scala-3.4.2, but do not activate it: scala-3.3.x is LTS version;


                        Pure: The Pure Isabelle System


This directory contains the ML source files for Pure Isabelle, which is
the basis for all object-logics. Building the Isabelle/Pure heap image
in batch mode works as follows:

  $ isabelle build Pure

To explore the bootstrap of Pure interactively, the Prover IDE can be
used like this:

  $ isabelle jedit -l Pure ROOT.ML

or alternatively the raw Poly/ML console:

  $ isabelle console -r
  Poly/ML> use "ROOT0.ML";
  Poly/ML> use "ROOT.ML";