equal
deleted
inserted
replaced
1 Pure: The Pure Isabelle System |
1 Pure: The Pure Isabelle System |
2 |
2 |
3 This directory contains the ML source files for Pure Isabelle, which is the |
3 This directory contains the ML source files for Pure Isabelle, which |
4 basis for all object-logics. Important files include: |
4 is the basis for all object-logics: |
5 |
5 |
6 IsaMakefile -- compiles the files |
6 IsaMakefile compiles the Pure system |
|
7 ML-Systems/ compatibility files for various ML systems |
|
8 Syntax/ the syntax module |
|
9 Thy/ the theory file parser and loader |
7 |
10 |
8 Syntax/ -- the syntax module |
11 Isabelle programmers may want to have a look at the following generic |
|
12 modules: |
9 |
13 |
10 Thy/ -- the theory file parser and loader |
14 Library basic library (see library.ML) |
11 |
15 TableFun efficient tables (see table.ML) |
12 ML-Systems/ -- compatibility files for various ML systems |
16 Seq unbounded sequences (see seq.ML) |
|
17 Pretty pretty printing module (see Syntax/pretty.ML) |
|
18 Scanner scanner toolbox (see Syntax/lexicon.ML) |
|
19 Path abstract algebra of file paths (see Thy/path.ML) |
|
20 File file system operations (see Thy/file.ML) |