1signature INST_EXISTENTIALS =
2sig
3  val tac : Proof.context -> term list -> int -> tactic
4end
5
6structure Inst_Existentials : INST_EXISTENTIALS =
7struct
8
9fun tac ctxt [] = TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI})
10  | tac ctxt (t :: ts) =
11      (TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI}))
12      THEN_ALL_NEW (TRY o (
13        let
14          val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)] @{thm HOL.exI}
15        in
16          resolve_tac ctxt [thm] THEN' tac ctxt ts
17        end))
18
19end