(* Until revision 10221, rewriting in hypotheses of the form "(fun x => phi(x)) t" with "t" not rewritable used to behave as a beta-normalization tactic instead of raising the expected message
"nothing to rewrite" *)
Goalforall b, S b = O -> (fun a => 0 = (S a)) b -> True. intros b H H0.
Fail rewrite H in H0. Abort.
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
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.
