|
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 |
|
|
12269
|
7 |
ProofContext (the key concept of Isar proof contexts)
|
|
|
8 |
Locale (proof contexts as mathematical structures)
|
|
|
9 |
Proof (the Isar/VM proof language interpreter)
|
|
7484
|
10 |
Args (concrete argument syntax of attributes and methods)
|
|
|
11 |
Method (proof methods)
|
|
|
12 |
Attrib (attributes)
|
|
|
13 |
|
|
|
14 |
LocalDefs (local definitions)
|
|
|
15 |
Calculation (calculational proofs)
|
|
11020
|
16 |
Obtain (generalized existence reasoning)
|
|
7484
|
17 |
|
|
|
18 |
Toplevel (the Isabelle/Isar toplevel)
|
|
|
19 |
IsarThy (Isar derived theory operations)
|
|
|
20 |
IsarCmd (non-logical commands)
|
|
|
21 |
IsarSyn (syntax for Pure/Isar commands)
|
|
|
22 |
|
|
|
23 |
OuterParse (outer syntax parser combinators, see also
|
|
|
24 |
Pure/General/scan.ML)
|
|
|
25 |
OuterSyntax (outer syntax main)
|
|
9124
|
26 |
IsarOutput (token-level theory output)
|