# HG changeset patch
# User wenzelm
# Date 1156870571 -7200
# Node ID fd646e926983b18b31c040cc8b62e16d585d1f41
# Parent  116255c9209b4db768c97ffdbb8928d71e4e68da
tuned;

diff -r 116255c9209b -r fd646e926983 doc-src/IsarImplementation/Thy/document/prelim.tex
--- 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
diff -r 116255c9209b -r fd646e926983 doc-src/IsarImplementation/Thy/prelim.thy
--- 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