src/Pure/README

discontinued obsolete "val extend = I" for data slots;

+
−
+
−                        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";