Theorem test (A:Prop) : A \/ A -> A.
Fail intro H; destruct H as H. (* Error: Disjunctive/conjunctive introduction pattern expected. *)
Fail intros H; destruct H as H. Abort.
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.
