--- 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 {*
--- 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%