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