|
7484
|
1 |
|
|
|
2 |
Pure/Isar/
|
|
|
3 |
|
|
|
4 |
This directory contains the Isabelle/Isar subsystem -- Intelligible
|
|
|
5 |
Semi-Automated Reasoning for Isabelle. Interesting modules include:
|
|
|
6 |
|
|
11020
|
7 |
ProofContext (structure of Isar proof contexts)
|
|
7484
|
8 |
Proof (core of the Isar/VM interpreter)
|
|
|
9 |
Args (concrete argument syntax of attributes and methods)
|
|
|
10 |
Method (proof methods)
|
|
|
11 |
Attrib (attributes)
|
|
|
12 |
|
|
|
13 |
LocalDefs (local definitions)
|
|
|
14 |
Calculation (calculational proofs)
|
|
11020
|
15 |
Obtain (generalized existence reasoning)
|
|
7484
|
16 |
|
|
|
17 |
Toplevel (the Isabelle/Isar toplevel)
|
|
|
18 |
IsarThy (Isar derived theory operations)
|
|
|
19 |
IsarCmd (non-logical commands)
|
|
|
20 |
IsarSyn (syntax for Pure/Isar commands)
|
|
|
21 |
|
|
|
22 |
OuterParse (outer syntax parser combinators, see also
|
|
|
23 |
Pure/General/scan.ML)
|
|
|
24 |
OuterSyntax (outer syntax main)
|
|
9124
|
25 |
IsarOutput (token-level theory output)
|