author | wenzelm |
Fri, 12 Aug 2022 19:47:38 +0200 | |
changeset 75827 | 4920ebbde486 |
parent 68630 | c55f6f0b3854 |
permissions | -rw-r--r-- |
signature INST_EXISTENTIALS = sig val tac : Proof.context -> term list -> int -> tactic end structure Inst_Existentials : INST_EXISTENTIALS = struct fun tac ctxt [] = TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI}) | tac ctxt (t :: ts) = (TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI})) THEN_ALL_NEW (TRY o ( let val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)] @{thm HOL.exI} in resolve_tac ctxt [thm] THEN' tac ctxt ts end)) end