author | blanchet |
Wed, 03 Nov 2010 22:33:23 +0100 | |
changeset 40342 | 3154f63e2bda |
parent 30834 | 1640e0625301 |
child 57440 | 802d33c46459 |
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 |
|
30834 | 18 |
isabelle tty -l RAW |
19 |
use "ROOT.ML"; |
|
16115 | 20 |