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

Two English errors fixed
author Adam Chlipala Sat, 15 Aug 2015 15:54:11 -0400 ed829eaa91b2 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.