section‹Tactic for instantiating existentials› theory Inst_Existentials imports Main begin
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. ›
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.
