clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;
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";