equal
deleted
inserted
replaced
2 Pure/Isar/ |
2 Pure/Isar/ |
3 |
3 |
4 This directory contains the Isabelle/Isar subsystem -- Intelligible |
4 This directory contains the Isabelle/Isar subsystem -- Intelligible |
5 Semi-Automated Reasoning for Isabelle. Interesting modules include: |
5 Semi-Automated Reasoning for Isabelle. Interesting modules include: |
6 |
6 |
7 ProofContext (structure of Isar proof contexts) |
7 ProofContext (the key concept of Isar proof contexts) |
8 Proof (core of the Isar/VM interpreter) |
8 Locale (proof contexts as mathematical structures) |
|
9 Proof (the Isar/VM proof language interpreter) |
9 Args (concrete argument syntax of attributes and methods) |
10 Args (concrete argument syntax of attributes and methods) |
10 Method (proof methods) |
11 Method (proof methods) |
11 Attrib (attributes) |
12 Attrib (attributes) |
12 |
13 |
13 LocalDefs (local definitions) |
14 LocalDefs (local definitions) |