diff src/Universes.v @ 392:4b1242b277b2

Typo fixes
author Adam Chlipala <adam@chlipala.net>
date Fri, 20 Apr 2012 12:49:47 -0400
parents 057a29f9c773
children 05efde66559d
line wrap: on
line diff
--- a/src/Universes.v	Thu Apr 12 18:46:55 2012 -0400
+++ b/src/Universes.v	Fri Apr 20 12:49:47 2012 -0400
@@ -627,7 +627,7 @@
 
 (** This kind of %``%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic.  However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming.
 
-   In general, there is a significant burden associated with any use of axioms.  It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%.   That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant.  For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)
+   In general, there is a significant burden associated with any use of axioms.  It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%.   That is, a set of axioms may imply [False], which allows any theorem to be proved, which defeats the purpose of a proof assistant.  For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)
 
 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.