equal
deleted
inserted
replaced
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{isar}% |
|
4 % |
|
5 \isadelimtheory |
|
6 \isanewline |
|
7 \isanewline |
|
8 \isanewline |
|
9 % |
|
10 \endisadelimtheory |
|
11 % |
|
12 \isatagtheory |
|
13 \isacommand{theory}\isamarkupfalse% |
|
14 \ isar\ \isakeyword{imports}\ base\ \isakeyword{begin}% |
|
15 \endisatagtheory |
|
16 {\isafoldtheory}% |
|
17 % |
|
18 \isadelimtheory |
|
19 % |
|
20 \endisadelimtheory |
|
21 % |
|
22 \isamarkupchapter{Isar proof texts% |
|
23 } |
|
24 \isamarkuptrue% |
|
25 % |
|
26 \isamarkupsection{Proof context% |
|
27 } |
|
28 \isamarkuptrue% |
|
29 % |
|
30 \begin{isamarkuptext}% |
|
31 FIXME% |
|
32 \end{isamarkuptext}% |
|
33 \isamarkuptrue% |
|
34 % |
|
35 \isamarkupsection{Proof state \label{sec:isar-proof-state}% |
|
36 } |
|
37 \isamarkuptrue% |
|
38 % |
|
39 \begin{isamarkuptext}% |
|
40 FIXME |
|
41 |
|
42 \glossary{Proof state}{The whole configuration of a structured proof, |
|
43 consisting of a \seeglossary{proof context} and an optional |
|
44 \seeglossary{structured goal}. Internally, an Isar proof state is |
|
45 organized as a stack to accomodate block structure of proof texts. |
|
46 For historical reasons, a low-level \seeglossary{tactical goal} is |
|
47 occasionally called ``proof state'' as well.} |
|
48 |
|
49 \glossary{Structured goal}{FIXME} |
|
50 |
|
51 \glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}% |
|
52 \end{isamarkuptext}% |
|
53 \isamarkuptrue% |
|
54 % |
|
55 \isamarkupsection{Proof methods% |
|
56 } |
|
57 \isamarkuptrue% |
|
58 % |
|
59 \begin{isamarkuptext}% |
|
60 FIXME% |
|
61 \end{isamarkuptext}% |
|
62 \isamarkuptrue% |
|
63 % |
|
64 \isamarkupsection{Attributes% |
|
65 } |
|
66 \isamarkuptrue% |
|
67 % |
|
68 \begin{isamarkuptext}% |
|
69 FIXME ?!% |
|
70 \end{isamarkuptext}% |
|
71 \isamarkuptrue% |
|
72 % |
|
73 \isadelimtheory |
|
74 % |
|
75 \endisadelimtheory |
|
76 % |
|
77 \isatagtheory |
|
78 \isacommand{end}\isamarkupfalse% |
|
79 % |
|
80 \endisatagtheory |
|
81 {\isafoldtheory}% |
|
82 % |
|
83 \isadelimtheory |
|
84 % |
|
85 \endisadelimtheory |
|
86 \isanewline |
|
87 \end{isabellebody}% |
|
88 %%% Local Variables: |
|
89 %%% mode: latex |
|
90 %%% TeX-master: "root" |
|
91 %%% End: |
|