clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
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";