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 |
|
|
9 |
isatool make Pure
|
|
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 |
|
16115
|
14 |
isatool make RAW
|
|
15 |
|
|
16 |
Now the Pure session may be compiled interactively as follows:
|
0
|
17 |
|
16115
|
18 |
isabelle -u RAW
|
|
19 |
|
16117
|
20 |
See ROOT.ML for further information.
|
16116
|
21 |
|
16115
|
22 |
|
|
23 |
$Id$
|