# HG changeset patch
# User wenzelm
# Date 1362054291 -3600
# Node ID 0e71a248cacbc22bdf13ba7c06d98a16d9c6d0f5
# Parent  4cca272150ab7c40e5e6ed5619518717059787f0
marginalized historic strip_tac;

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"} \\
diff -r 4cca272150ab -r 0e71a248cacb src/HOL/Bali/Basis.thy
--- 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]
diff -r 4cca272150ab -r 0e71a248cacb src/HOL/HOL.thy
--- 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
diff -r 4cca272150ab -r 0e71a248cacb src/HOL/MicroJava/J/JTypeSafe.thy
--- 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])")