--- a/doc-src/IsarRef/Thy/document/Proof.tex Sun Feb 15 18:54:50 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Sun Feb 15 18:56:13 2009 +0100
@@ -3,8 +3,6 @@
\def\isabellecontext{Proof}%
%
\isadelimtheory
-\isanewline
-\isanewline
%
\endisadelimtheory
%
@@ -20,7 +18,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Proofs%
+\isamarkupchapter{Proofs \label{ch:proofs}%
}
\isamarkuptrue%
%
@@ -28,8 +26,8 @@
Proof commands perform transitions of Isar/VM machine
configurations, which are block-structured, consisting of a stack of
nodes with three main components: logical proof context, current
- facts, and open goals. Isar/VM transitions are \emph{typed}
- according to the following three different modes of operation:
+ facts, and open goals. Isar/VM transitions are typed according to
+ the following three different modes of operation:
\begin{description}
@@ -49,13 +47,17 @@
\end{description}
- The proof mode indicator may be read as a verb telling the writer
- what kind of operation may be performed next. The corresponding
- typings of proof commands restricts the shape of well-formed proof
- texts to particular command sequences. So dynamic arrangements of
- commands eventually turn out as static texts of a certain structure.
- \Appref{ap:refcard} gives a simplified grammar of the overall
- (extensible) language emerging that way.%
+ The proof mode indicator may be understood as an instruction to the
+ writer, telling what kind of operation may be performed next. The
+ corresponding typings of proof commands restricts the shape of
+ well-formed proof texts to particular command sequences. So dynamic
+ arrangements of commands eventually turn out as static texts of a
+ certain structure.
+
+ \Appref{ap:refcard} gives a simplified grammar of the (extensible)
+ language emerging that way from the different types of proof
+ commands. The main ideas of the overall Isar framework are
+ explained in \chref{ch:isar-framework}.%
\end{isamarkuptext}%
\isamarkuptrue%
%