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/Relations/Relations.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'theories/Relations/Relations.v')

diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index f792e4c2a7..d2c3e2776c 100755
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -12,17 +12,17 @@ Require Export Relation_Definitions.
 Require Export Relation_Operators.
 Require Export Operators_Properties.
 
-Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B)
-  (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))).
-Intros; Split; Elim H; Red; Auto.
-Intros _ equiv_trans _ x y z H0 H1; Apply equiv_trans with (f y); Assumption.
+Lemma inverse_image_of_equivalence :
+ forall (A B:Set) (f:A -> B) (r:relation B),
+   equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
+intros; split; elim H; red in |- *; auto.
+intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
-Lemma inverse_image_of_eq : (A,B:Set)(f:A->B)
-  (equivalence A [x,y:A](f x)=(f y)).
-Split; Red;
-[ (* reflexivity *)  Reflexivity
-| (* transitivity *) Intros; Transitivity (f y); Assumption
-| (* symmetry *) Intros; Symmetry; Assumption
-].
-Qed.
+Lemma inverse_image_of_eq :
+ forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+split; red in |- *;
+ [  (* reflexivity *) reflexivity
+ |  (* transitivity *) intros; transitivity (f y); assumption
+ |  (* symmetry *) intros; symmetry  in |- *; assumption ].
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3