equal
deleted
inserted
replaced
1 |
|
2 (* $Id$ *) |
|
3 |
|
4 theory isar imports base begin |
|
5 |
|
6 chapter {* Isar proof texts *} |
|
7 |
|
8 section {* Proof context *} |
|
9 |
|
10 text FIXME |
|
11 |
|
12 |
|
13 section {* Proof state \label{sec:isar-proof-state} *} |
|
14 |
|
15 text {* |
|
16 FIXME |
|
17 |
|
18 \glossary{Proof state}{The whole configuration of a structured proof, |
|
19 consisting of a \seeglossary{proof context} and an optional |
|
20 \seeglossary{structured goal}. Internally, an Isar proof state is |
|
21 organized as a stack to accomodate block structure of proof texts. |
|
22 For historical reasons, a low-level \seeglossary{tactical goal} is |
|
23 occasionally called ``proof state'' as well.} |
|
24 |
|
25 \glossary{Structured goal}{FIXME} |
|
26 |
|
27 \glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage} |
|
28 |
|
29 |
|
30 *} |
|
31 |
|
32 section {* Proof methods *} |
|
33 |
|
34 text FIXME |
|
35 |
|
36 section {* Attributes *} |
|
37 |
|
38 text "FIXME ?!" |
|
39 |
|
40 |
|
41 end |
|