--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu Aug 31 23:01:16 2006 +0200
@@ -23,7 +23,7 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Local variables%
+\isamarkupsection{Variables and schematic polymorphism%
}
\isamarkuptrue%
%
@@ -101,15 +101,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Schematic polymorphism%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Assumptions%
}
\isamarkuptrue%
@@ -128,7 +119,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Structured proofs \label{sec:isar-proof-state}%
+\isamarkupsection{Proof states \label{sec:isar-proof-state}%
}
\isamarkuptrue%
%