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