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