## Mercurial > cpdt > repo

### diff src/LogicProg.v @ 539:8dddcaaeb67a

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Two English errors fixed

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Sat, 15 Aug 2015 15:54:11 -0400 |

parents | ed829eaa91b2 |

children | 582bf8d4ce51 |

line wrap: on

line diff

--- a/src/LogicProg.v Wed Aug 05 18:19:59 2015 -0400 +++ b/src/LogicProg.v Sat Aug 15 15:54:11 2015 -0400 @@ -398,7 +398,7 @@ Hint Resolve eq_trans : slow. (* end thide *) -Example three_minus_four_zero : exists x, 1 + x = 0. +Example from_one_to_zero : exists x, 1 + x = 0. (* begin thide *) Time eauto. (** %\vspace{-.15in}% @@ -777,7 +777,7 @@ Hint Resolve plus_0 times_1. -(** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) +(** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) Require Import Arith Ring.