author | ballarin |
Mon, 19 Jan 2009 20:37:08 +0100 | |
changeset 29566 | 937baa077df2 |
parent 28504 | 7ad7d7d6df47 |
child 30204 | 8ede2f7104cf |
permissions | -rw-r--r-- |
4689 | 1 |
|
19 | 2 |
Pure: The Pure Isabelle System |
0 | 3 |
|
4689 | 4 |
|
4620 | 5 |
This directory contains the ML source files for Pure Isabelle, which |
16115 | 6 |
is the basis for all object-logics. The Isabelle/Pure image may be |
7 |
compiled in batch mode like this: |
|
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 | 10 |
|
11 |
Developers may want to produce a RAW image that merely consists of the |
|
12 |
ML compiler with the compatibility setup of ML-Systems/ preloaded: |
|
0 | 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 | 15 |
|
16 |
Now the Pure session may be compiled interactively as follows: |
|
0 | 17 |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
16117
diff
changeset
|
18 |
isabelle-process -u RAW |
16115 | 19 |
|
16117 | 20 |
See ROOT.ML for further information. |
16116 | 21 |
|
16115 | 22 |
|
23 |
$Id$ |