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