diff options
Diffstat (limited to 'theories/Sets')
-rwxr-xr-x | theories/Sets/Classical_sets.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Constructive_sets.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Cpo.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Ensembles.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Finite_sets.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Finite_sets_facts.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Image.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Infinite_sets.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Integers.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Multiset.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Partial_Order.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Permut.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Powerset.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Powerset_Classical_facts.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Powerset_facts.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Relations_1.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Relations_1_facts.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Relations_2.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Relations_2_facts.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Relations_3.v | 14 | ||||
-rwxr-xr-x | theories/Sets/Relations_3_facts.v | 14 | ||||
-rw-r--r-- | theories/Sets/Uniset.v | 14 |
22 files changed, 154 insertions, 154 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index e2d707367..a21534bd5 100755 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index b4250be92..09a941bcd 100755 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 59f8fb2c8..efd83c106 100755 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index eae50a3d1..9c85d67d0 100755 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index dce4c64e8..53981ea8d 100755 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index f394b2e5a..94ea964c2 100755 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index fd1c90b90..469b41783 100755 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index d401b86c1..c3492ba78 100755 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index c9121032d..970d6dab1 100755 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index a3ae98d0a..aad294e93 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) +(************************************************************************) (*i $Id$ i*) diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 15fc690dd..07244e66f 100755 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index c3a1da01c..006831909 100755 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) +(************************************************************************) (*i $Id$ i*) diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 543702276..c323ca356 100755 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 71ec5b078..1ac59056b 100755 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 91018f05e..cae796861 100755 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 16a00740d..f15bf19e6 100755 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 61557aff7..fd83b0e0d 100755 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index d7ee68b66..918e45ee1 100755 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 2a0aaf98b..a7da7db9a 100755 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index d84884d41..d6202cffe 100755 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 5b1ce9e31..d8bf7dc3c 100755 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index e1ba00209..03dc55ef9 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* 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 *) +(************************************************************************) (*i $Id$ i*) |