diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Sets/Relations_1.v | |
parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) |
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
Diffstat (limited to 'theories/Sets/Relations_1.v')
-rwxr-xr-x | theories/Sets/Relations_1.v | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 74c031726..16a00740d 100755 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -27,41 +27,41 @@ (*i $Id$ i*) Section Relations_1. - Variable U: Type. + Variable U : Type. - Definition Relation := U -> U -> Prop. - Variable R: Relation. + Definition Relation := U -> U -> Prop. + Variable R : Relation. - Definition Reflexive : Prop := (x: U) (R x x). + Definition Reflexive : Prop := forall x:U, R x x. - Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z). + Definition Transitive : Prop := forall x y z:U, R x y -> R y z -> R x z. - Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x). + Definition Symmetric : Prop := forall x y:U, R x y -> R y x. - Definition Antisymmetric : Prop := - (x: U) (y: U) (R x y) -> (R y x) -> x == y. + Definition Antisymmetric : Prop := forall x y:U, R x y -> R y x -> x = y. - Definition contains : Relation -> Relation -> Prop := - [R,R': Relation] (x: U) (y: U) (R' x y) -> (R x y). + Definition contains (R R':Relation) : Prop := + forall x y:U, R' x y -> R x y. - Definition same_relation : Relation -> Relation -> Prop := - [R,R': Relation] (contains R R') /\ (contains R' R). + Definition same_relation (R R':Relation) : Prop := + contains R R' /\ contains R' R. Inductive Preorder : Prop := - Definition_of_preorder: Reflexive -> Transitive -> Preorder. + Definition_of_preorder : Reflexive -> Transitive -> Preorder. Inductive Order : Prop := - Definition_of_order: Reflexive -> Transitive -> Antisymmetric -> Order. + Definition_of_order : + Reflexive -> Transitive -> Antisymmetric -> Order. Inductive Equivalence : Prop := - Definition_of_equivalence: - Reflexive -> Transitive -> Symmetric -> Equivalence. + Definition_of_equivalence : + Reflexive -> Transitive -> Symmetric -> Equivalence. Inductive PER : Prop := - Definition_of_PER: Symmetric -> Transitive -> PER. + Definition_of_PER : Symmetric -> Transitive -> PER. End Relations_1. -Hints Unfold Reflexive Transitive Antisymmetric Symmetric contains - same_relation : sets v62. -Hints Resolve Definition_of_preorder Definition_of_order - Definition_of_equivalence Definition_of_PER : sets v62. +Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains + same_relation: sets v62. +Hint Resolve Definition_of_preorder Definition_of_order + Definition_of_equivalence Definition_of_PER: sets v62.
\ No newline at end of file |