diff -r 4cca272150ab -r 0e71a248cacb src/Doc/IsarRef/ML_Tactic.thy
--- a/src/Doc/IsarRef/ML_Tactic.thy	Thu Feb 28 13:19:25 2013 +0100
+++ b/src/Doc/IsarRef/ML_Tactic.thy	Thu Feb 28 13:24:51 2013 +0100
@@ -119,7 +119,6 @@
   \begin{tabular}{lll}
     @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
     @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
-    @{ML strip_tac}~@{text 1} & @{text "\<approx>"} & @{text "intro strip"} \\
     @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
       & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
       & @{text "\<lless>"} & @{text "clarify"} \\