From f82bfc64fca9fb46136d7aa26c09d64cde0432d2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 2 Jun 2008 23:26:13 +0000
Subject: In abstract parts of theories/Numbers, plus/times becomes add/mul,
 for increased consistency with bignums parts

(commit part I: content of files)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'theories/Numbers/Integer/SpecViaZ')

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 3d9d3d1901..bb56e6997c 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -41,9 +41,9 @@ Definition NZeq := Z.eq.
 Definition NZ0 := Z.zero.
 Definition NZsucc := Z.succ.
 Definition NZpred := Z.pred.
-Definition NZplus := Z.add.
+Definition NZadd := Z.add.
 Definition NZminus := Z.sub.
-Definition NZtimes := Z.mul.
+Definition NZmul := Z.mul.
 
 Theorem NZeq_equiv : equiv Z.t Z.eq.
 Proof.
@@ -66,7 +66,7 @@ Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
 
-Add Morphism NZplus with signature Z.eq ==> Z.eq ==> Z.eq as NZplus_wd.
+Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd.
 Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
@@ -76,7 +76,7 @@ Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
 
-Add Morphism NZtimes with signature Z.eq ==> Z.eq ==> Z.eq as NZtimes_wd.
+Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd.
 Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
@@ -144,12 +144,12 @@ Qed.
 
 End Induction.
 
-Theorem NZplus_0_l : forall n, 0 + n == n.
+Theorem NZadd_0_l : forall n, 0 + n == n.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZplus_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
+Theorem NZadd_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m).
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
@@ -164,12 +164,12 @@ Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZtimes_0_l : forall n, 0 * n == 0.
+Theorem NZmul_0_l : forall n, 0 * n == 0.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m, (Z.succ n) * m == n * m + m.
+Theorem NZmul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
 Proof.
 intros; zsimpl; ring.
 Qed.
-- 
cgit v1.2.3