src/Pure/README
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 16117 7c7da01ff77e
child 28504 7ad7d7d6df47
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
wenzelm@4689
     1
wenzelm@19
     2
                        Pure: The Pure Isabelle System
clasohm@0
     3
wenzelm@4689
     4
wenzelm@4620
     5
This directory contains the ML source files for Pure Isabelle, which
wenzelm@16115
     6
is the basis for all object-logics.  The Isabelle/Pure image may be
wenzelm@16115
     7
compiled in batch mode like this:
wenzelm@16115
     8
wenzelm@16115
     9
  isatool make Pure
wenzelm@16115
    10
wenzelm@16115
    11
Developers may want to produce a RAW image that merely consists of the
wenzelm@16115
    12
ML compiler with the compatibility setup of ML-Systems/ preloaded:
clasohm@0
    13
wenzelm@16115
    14
  isatool make RAW
wenzelm@16115
    15
wenzelm@16115
    16
Now the Pure session may be compiled interactively as follows:
clasohm@0
    17
wenzelm@16115
    18
  isabelle -u RAW
wenzelm@16115
    19
wenzelm@16117
    20
See ROOT.ML for further information.
wenzelm@16116
    21
wenzelm@16115
    22
wenzelm@16115
    23
$Id$