Ltac induction_last := let v := matchgoalwith
| |- forall x y, _ = _ -> _ => 1
| |- forall x y, _ -> _ = _ -> _ => 2
| |- forall x y, _ -> _ -> _ = _ -> _ => 3 end in induction v.
Goalforall n m : nat, True -> n = m -> m = n.
induction_last. reflexivity. Qed.
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.
