1structure jcLib :> jcLib =
2struct
3
4open HolKernel boolLib Abbrev Tactic Tactical BasicProvers simpLib
5open Rewrite bossLib Thm_cont
6
7(* existing strip_tac looks like
8
9    gen_tac ORELSE conj_tac ORELSE disch_then strip_assume_tac
10
11*)
12
13(* disch_then : thm_tactic -> tactic
14     =          (thm -> tactic) -> tactic
15*)
16
17fun stripDup ths =
18    FIRST [gen_tac, conj_tac,
19           disch_then (fn th => strip_assume_tac th >>
20                                strip_assume_tac (REWRITE_RULE ths th))]
21
22
23
24end