signature INST_EX_ASSN = sig val tac : Proof.context -> term list -> int -> tactic end structure Inst_Ex_Assn : INST_EX_ASSN = struct fun tac ctxt [] = TRY o REPEAT_ALL_NEW (assume_tac ctxt) | tac ctxt (t :: ts) = (TRY o ( let val thm = Drule.infer_instantiate' ctxt [NONE, NONE, SOME (Thm.cterm_of ctxt t)] @{thm Assertions.ent_ex_postI} in resolve_tac ctxt [thm] THEN' tac ctxt ts end)) end