section‹Tactic for instantiating existentials› theory Inst_Ex_Assn imports Separation_Logic_Imperative_HOL.Assertions begin
thm ent_ex_postI
text‹
Coinduction proofs in Isabelle often lead to proof obligations with nested conjunctions and
existential quantifiers, e.g. prop‹∃x y. P x y ∧ (∃z. Q x y z)› .
The following tactic allows instantiating these existentials with a given list of witnesses.
This tactic was adjusted to work with the assertion specific prop‹∃A› ›
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 und die Messung sind noch experimentell.
