From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Nov 2003 17:28:49 +0000
Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et
 states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Peano_dec.v | 26 ++++++++++++--------------
 1 file changed, 12 insertions(+), 14 deletions(-)

(limited to 'theories/Arith/Peano_dec.v')

diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 96a8523f9f..4d657d0602 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -8,29 +8,27 @@
 
 (*i $Id$ i*)
 
-Require Decidable.
+Require Import Decidable.
 
-V7only [Import nat_scope.].
 Open Local Scope nat_scope.
 
-Implicit Variables Type m,n,x,y:nat.
+Implicit Types m n x y : nat.
 
-Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
+Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}.
 Proof.
-NewInduction n.
-Auto.
-Left; Exists n; Auto.
+induction n.
+auto.
+left; exists n; auto.
 Defined.
 
-Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}.
+Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
 Proof.
-NewInduction n; NewInduction m; Auto.
-Elim (IHn m); Auto.
+induction n; induction m; auto.
+elim (IHn m); auto.
 Defined.
 
-Hints Resolve O_or_S eq_nat_dec : arith.
+Hint Resolve O_or_S eq_nat_dec: arith.
 
-Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
-Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
+Theorem dec_eq_nat : forall n m, decidable (n = m).
+intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith.
 Defined.
-
-- 
cgit v1.2.3