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
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|