src/Pure/README
author blanchet
Wed, 03 Nov 2010 22:33:23 +0100
changeset 40342 3154f63e2bda
parent 30834 1640e0625301
child 57440 802d33c46459
permissions -rw-r--r--
don't be overly verbose in Sledgehammer's minimizer
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
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 16117
diff changeset
     9
  isabelle make Pure
16115
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
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 16117
diff changeset
    14
  isabelle make RAW
16115
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
30834
1640e0625301 tuned comments;
wenzelm
parents: 30204
diff changeset
    18
  isabelle tty -l RAW
1640e0625301 tuned comments;
wenzelm
parents: 30204
diff changeset
    19
  use "ROOT.ML";
16115
wenzelm
parents: 6127
diff changeset
    20