equal
deleted
inserted
replaced
1 |
1 |
2 Pure: The Pure Isabelle System |
2 Pure: The Pure Isabelle System |
3 |
3 |
4 |
4 |
5 This directory contains the ML source files for Pure Isabelle, which |
5 This directory contains the ML source files for Pure Isabelle, which |
6 is the basis for all object-logics: |
6 is the basis for all object-logics. The Isabelle/Pure image may be |
|
7 compiled in batch mode like this: |
7 |
8 |
8 IsaMakefile compiles the Pure system (use isatool make) |
9 isatool make Pure |
9 ML-Systems/ compatibility files for various ML systems |
|
10 General/ general tools |
|
11 Syntax/ the syntax module |
|
12 Thy/ the theory file parser (old format) and loader |
|
13 Isar/ Intelligible Semi-Automated Reasoning subsystem |
|
14 ./ the actual meta logic implementation (see ROOT.ML) |
|
15 |
10 |
16 Isabelle programmers may want to have a look at the generic modules |
11 Developers may want to produce a RAW image that merely consists of the |
17 Library (see library.ML) and those in General/ (see General/README). |
12 ML compiler with the compatibility setup of ML-Systems/ preloaded: |
|
13 |
|
14 isatool make RAW |
|
15 |
|
16 Now the Pure session may be compiled interactively as follows: |
|
17 |
|
18 isabelle -u RAW |
|
19 |
|
20 |
|
21 $Id$ |