src/Pure/README
author wenzelm
Fri, 21 Sep 2007 22:51:08 +0200
changeset 24669 4579eac2c997
parent 16117 7c7da01ff77e
child 28504 7ad7d7d6df47
permissions -rw-r--r--
proper signature constraint; minor tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4689
wenzelm
parents: 4620
diff changeset
     1
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
     2
                        Pure: The Pure Isabelle System
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
4689
wenzelm
parents: 4620
diff changeset
     4
4620
bfd40126c56e improved comments;
wenzelm
parents: 3279
diff changeset
     5
This directory contains the ML source files for Pure Isabelle, which
16115
wenzelm
parents: 6127
diff changeset
     6
is the basis for all object-logics.  The Isabelle/Pure image may be
wenzelm
parents: 6127
diff changeset
     7
compiled in batch mode like this:
wenzelm
parents: 6127
diff changeset
     8
wenzelm
parents: 6127
diff changeset
     9
  isatool make Pure
wenzelm
parents: 6127
diff changeset
    10
wenzelm
parents: 6127
diff changeset
    11
Developers may want to produce a RAW image that merely consists of the
wenzelm
parents: 6127
diff changeset
    12
ML compiler with the compatibility setup of ML-Systems/ preloaded:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
16115
wenzelm
parents: 6127
diff changeset
    14
  isatool make RAW
wenzelm
parents: 6127
diff changeset
    15
wenzelm
parents: 6127
diff changeset
    16
Now the Pure session may be compiled interactively as follows:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
16115
wenzelm
parents: 6127
diff changeset
    18
  isabelle -u RAW
wenzelm
parents: 6127
diff changeset
    19
16117
wenzelm
parents: 16116
diff changeset
    20
See ROOT.ML for further information.
16116
wenzelm
parents: 16115
diff changeset
    21
16115
wenzelm
parents: 6127
diff changeset
    22
wenzelm
parents: 6127
diff changeset
    23
$Id$