diff options
author | 2005-12-26 13:59:13 +0000 | |
---|---|---|
committer | 2005-12-26 13:59:13 +0000 | |
commit | f6e1acbbe00aeb479fde229c3941e3a6a2d53068 (patch) | |
tree | ce3a6476de30cbf68c7668f5ecba92f457a721e8 /theories7/Sets/Relations_3.v | |
parent | e0f9487be5ce770117a9c9c815af8c7010ff357b (diff) |
Suppression des fichiers .v en ancienne syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7/Sets/Relations_3.v')
-rwxr-xr-x | theories7/Sets/Relations_3.v | 63 |
1 files changed, 0 insertions, 63 deletions
diff --git a/theories7/Sets/Relations_3.v b/theories7/Sets/Relations_3.v deleted file mode 100755 index 204f838f7..000000000 --- a/theories7/Sets/Relations_3.v +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(****************************************************************************) -(* *) -(* Naive Set Theory in Coq *) -(* *) -(* INRIA INRIA *) -(* Rocquencourt Sophia-Antipolis *) -(* *) -(* Coq V6.1 *) -(* *) -(* Gilles Kahn *) -(* Gerard Huet *) -(* *) -(* *) -(* *) -(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) -(* to the Newton Institute for providing an exceptional work environment *) -(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) -(****************************************************************************) - -(*i $Id$ i*) - -Require Export Relations_1. -Require Export Relations_2. - -Section Relations_3. - Variable U: Type. - Variable R: (Relation U). - - Definition coherent : U -> U -> Prop := - [x,y: U] (EXT z | (Rstar U R x z) /\ (Rstar U R y z)). - - Definition locally_confluent : U -> Prop := - [x: U] (y,z: U) (R x y) -> (R x z) -> (coherent y z). - - Definition Locally_confluent : Prop := (x: U) (locally_confluent x). - - Definition confluent : U -> Prop := - [x: U] (y,z: U) (Rstar U R x y) -> (Rstar U R x z) -> (coherent y z). - - Definition Confluent : Prop := (x: U) (confluent x). - - Inductive noetherian : U -> Prop := - definition_of_noetherian: - (x: U) ((y: U) (R x y) -> (noetherian y)) -> (noetherian x). - - Definition Noetherian : Prop := (x: U) (noetherian x). - -End Relations_3. -Hints Unfold coherent : sets v62. -Hints Unfold locally_confluent : sets v62. -Hints Unfold confluent : sets v62. -Hints Unfold Confluent : sets v62. -Hints Resolve definition_of_noetherian : sets v62. -Hints Unfold Noetherian : sets v62. - - |