--- 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"} \\
--- a/src/HOL/Bali/Basis.thy Thu Feb 28 13:19:25 2013 +0100
+++ b/src/HOL/Bali/Basis.thy Thu Feb 28 13:24:51 2013 +0100
@@ -9,6 +9,8 @@
section "misc"
+ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
+
declare split_if_asm [split] option.split [split] option.split_asm [split]
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
--- a/src/HOL/HOL.thy Thu Feb 28 13:19:25 2013 +0100
+++ b/src/HOL/HOL.thy Thu Feb 28 13:24:51 2013 +0100
@@ -1987,8 +1987,6 @@
subsection {* Legacy tactics and ML bindings *}
ML {*
-fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
-
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
local
fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Feb 28 13:19:25 2013 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Feb 28 13:24:51 2013 +0100
@@ -198,7 +198,7 @@
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
apply( simp_all)
-apply( tactic "ALLGOALS strip_tac")
+apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")