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