equal
deleted
inserted
replaced
1 |
1 |
2 (* $Id$ *) |
2 (* $Id$ *) |
3 |
3 |
4 theory "proof" imports base begin |
4 theory "proof" imports base begin |
5 |
5 |
6 chapter {* Structured reasoning *} |
6 chapter {* Structured proofs *} |
7 |
7 |
8 section {* Proof context *} |
8 section {* Local variables *} |
9 |
|
10 subsection {* Local variables *} |
|
11 |
9 |
12 text FIXME |
10 text FIXME |
13 |
11 |
14 text %mlref {* |
12 text %mlref {* |
15 \begin{mldecls} |
13 \begin{mldecls} |
64 \end{description} |
62 \end{description} |
65 *} |
63 *} |
66 |
64 |
67 text FIXME |
65 text FIXME |
68 |
66 |
69 section {* Proof state *} |
67 |
|
68 section {* Schematic polymorphism *} |
|
69 |
|
70 text FIXME |
|
71 |
|
72 |
|
73 section {* Assumptions *} |
|
74 |
|
75 text FIXME |
|
76 |
|
77 |
|
78 section {* Conclusions *} |
|
79 |
|
80 text FIXME |
|
81 |
|
82 |
|
83 section {* Structured proofs \label{sec:isar-proof-state} *} |
70 |
84 |
71 text {* |
85 text {* |
72 FIXME |
86 FIXME |
73 |
87 |
74 \glossary{Proof state}{The whole configuration of a structured proof, |
88 \glossary{Proof state}{The whole configuration of a structured proof, |
83 \glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage} |
97 \glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage} |
84 |
98 |
85 |
99 |
86 *} |
100 *} |
87 |
101 |
88 section {* Methods *} |
102 section {* Proof methods *} |
89 |
103 |
90 text FIXME |
104 text FIXME |
91 |
105 |
92 section {* Attributes *} |
106 section {* Attributes *} |
93 |
107 |
94 text FIXME |
108 text "FIXME ?!" |
95 |
109 |
96 end |
110 end |