src/Pure/README
author nipkow
Tue, 02 Sep 2008 21:31:28 +0200
changeset 28091 50f2d6ba024c
parent 16117 7c7da01ff77e
child 28504 7ad7d7d6df47
permissions -rw-r--r--
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and distributed them over Real/ (to do with bijections and density). Library/NatPair became Nat_Int_Bij and made that part of Main.


                        Pure: The Pure Isabelle System


This directory contains the ML source files for Pure Isabelle, which
is the basis for all object-logics.  The Isabelle/Pure image may be
compiled in batch mode like this:

  isatool make Pure

Developers may want to produce a RAW image that merely consists of the
ML compiler with the compatibility setup of ML-Systems/ preloaded:

  isatool make RAW

Now the Pure session may be compiled interactively as follows:

  isabelle -u RAW

See ROOT.ML for further information.


$Id$