Tactic Notation"epose" open_constr(a) := let a' := fresh in pose a as a'.
Tactic Notation"epose2" open_constr(a) tactic3(tac) := let a' := fresh in pose a as a'. Goal True.
epose _. Undo.
epose2 _ idtac. 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.
