1 2 Pure: The Pure Isabelle System 3 4 5This directory contains the ML source files for Pure Isabelle, which is 6the basis for all object-logics. Building the Isabelle/Pure heap image 7in batch mode works as follows: 8 9 $ isabelle build Pure 10 11To explore the bootstrap of Pure interactively, the Prover IDE can be 12used like this: 13 14 $ isabelle jedit -l Pure ROOT.ML 15 16or alternatively the raw Poly/ML console: 17 18 $ isabelle console -r 19 Poly/ML> use "ROOT0.ML"; 20 Poly/ML> use "ROOT.ML"; 21