--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Aug 29 18:49:33 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Aug 29 18:56:11 2006 +0200
@@ -382,6 +382,24 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsubsection{Proof context \label{sec:context-proof}%
}
\isamarkuptrue%
@@ -419,10 +437,51 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsubsection{Generic contexts%
}
\isamarkuptrue%
%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarImplementation/Thy/prelim.thy Tue Aug 29 18:49:33 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Tue Aug 29 18:56:11 2006 +0200
@@ -313,6 +313,9 @@
FIXME theory data
*}
+text %mlref {*
+*}
+
subsection {* Proof context \label{sec:context-proof} *}
@@ -350,7 +353,13 @@
*}
+text %mlref {* FIXME *}
+
subsection {* Generic contexts *}
+text FIXME
+
+text %mlref {* FIXME *}
+
end