Ltac break_tuple := matchgoalwith
| [ H: context[match ?a with | pair n m => _ end] |- _ ] => let n := fresh n in let m := fresh m in destruct a as [n m] end.
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.
