|
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
|
|
|
6 |
is the basis for all object-logics:
|
|
0
|
7 |
|
|
4689
|
8 |
IsaMakefile compiles the Pure system (use isatool make)
|
|
4620
|
9 |
ML-Systems/ compatibility files for various ML systems
|
|
5020
|
10 |
General/ general tools
|
|
4620
|
11 |
Syntax/ the syntax module
|
|
6127
|
12 |
Thy/ the theory file parser (old format) and loader
|
|
5833
|
13 |
Isar/ Intelligible Semi-Automated Reasoning subsystem
|
|
4689
|
14 |
./ the actual meta logic implementation (see ROOT.ML)
|
|
0
|
15 |
|
|
6127
|
16 |
Isabelle programmers may want to have a look at the generic modules
|
|
|
17 |
Library (see library.ML) and those in General/ (see General/README).
|