# HG changeset patch
# User wenzelm
# Date 1327612893 -3600
# Node ID 4ab175c85d570ac2f123dceecf219b4b6951f09a
# Parent  e7518167215087f500ddc9b257a3ba1e58f2477f
tuned sectioning;

diff -r e75181672150 -r 4ab175c85d57 doc-src/IsarImplementation/Thy/Tactic.thy
--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Thu Jan 26 22:16:45 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Thu Jan 26 22:21:33 2012 +0100
@@ -642,6 +642,8 @@
   given tactic.  *}
 
 
+text %mlref ""
+
 subsubsection {* Filtering a tactic's results *}
 
 text {*
diff -r e75181672150 -r 4ab175c85d57 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 22:16:45 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 22:21:33 2012 +0100
@@ -798,6 +798,24 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
 \isamarkupsubsubsection{Filtering a tactic's results%
 }
 \isamarkuptrue%