| author | blanchet | 
| Tue, 22 Jun 2010 19:10:12 +0200 | |
| changeset 37508 | f9af8a863bd3 | 
| 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  |