Ltac foo := idtac.
Ltac bar H := idtac.
Goal True.
Proof.
Fail foo H.
Fail foo H H'.
Fail bar H H'.
Fail bar H H' H''.
Abort.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|