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