--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu Aug 31 22:55:49 2006 +0200
@@ -19,15 +19,11 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Structured reasoning%
+\isamarkupchapter{Structured proofs%
}
\isamarkuptrue%
%
-\isamarkupsection{Proof context%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Local variables%
+\isamarkupsection{Local variables%
}
\isamarkuptrue%
%
@@ -105,7 +101,34 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Proof state%
+\isamarkupsection{Schematic polymorphism%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Assumptions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Conclusions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Structured proofs \label{sec:isar-proof-state}%
}
\isamarkuptrue%
%
@@ -125,7 +148,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Methods%
+\isamarkupsection{Proof methods%
}
\isamarkuptrue%
%
@@ -139,7 +162,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+FIXME ?!%
\end{isamarkuptext}%
\isamarkuptrue%
%