section \<open>Tactic for instantiating existentials\<close> theory Inst_Existentials imports Main begin
text\<open>
Coinduction proofs in Isabelle often lead toproof obligations with nested conjunctions and
existential quantifiers, e.g. \<^prop>\<open>\<exists>x y. P x y \<and> (\<exists>z. Q x y z)\<close> .
The following tactic allows instantiating these existentials with a given list of witnesses. \<close>
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.
