Mercurial > cpdt > repo
changeset 540:582bf8d4ce51
Fuller English fix
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 15 Aug 2015 15:59:02 -0400 |
parents | 8dddcaaeb67a |
children | 429e95d23b26 |
files | src/LogicProg.v |
diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/LogicProg.v Sat Aug 15 15:54:11 2015 -0400 +++ b/src/LogicProg.v Sat Aug 15 15:59:02 2015 -0400 @@ -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 semiring, 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 _semiring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) Require Import Arith Ring.