1 files changed, 19 insertions, 19 deletions
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index c38a2fe1..0fa9c74a 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -24,27 +24,27 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Ensembles.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Section Ensembles.
   Variable U : Type.
-  
-  Definition Ensemble := U -> Prop. 
+
+  Definition Ensemble := U -> Prop.
 
   Definition In (A:Ensemble) (x:U) : Prop := A x.
-  
+
   Definition Included (B C:Ensemble) : Prop := forall x:U, In B x -> In C x.
-  
+
   Inductive Empty_set : Ensemble :=.
-  
+
   Inductive Full_set : Ensemble :=
     Full_intro : forall x:U, In Full_set x.
 
-(** NB: The following definition builds-in equality of elements in [U] as 
-     Leibniz equality. 
+(** NB: The following definition builds-in equality of elements in [U] as
+     Leibniz equality.
 
-     This may have to be changed if we replace [U] by a Setoid on [U] 
-     with its own equality [eqs], with  
+     This may have to be changed if we replace [U] by a Setoid on [U]
+     with its own equality [eqs], with
      [In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y)]. *)
 
   Inductive Singleton (x:U) : Ensemble :=
@@ -55,7 +55,7 @@ Section Ensembles.
     | Union_intror : forall x:U, In C x -> In (Union B C) x.
 
   Definition Add (B:Ensemble) (x:U) : Ensemble := Union B (Singleton x).
-  
+
   Inductive Intersection (B C:Ensemble) : Ensemble :=
     Intersection_intro :
     forall x:U, In B x -> In C x -> In (Intersection B C) x.
@@ -63,29 +63,29 @@ Section Ensembles.
   Inductive Couple (x y:U) : Ensemble :=
     | Couple_l : In (Couple x y) x
     | Couple_r : In (Couple x y) y.
-  
+
   Inductive Triple (x y z:U) : Ensemble :=
     | Triple_l : In (Triple x y z) x
     | Triple_m : In (Triple x y z) y
     | Triple_r : In (Triple x y z) z.
-  
+
   Definition Complement (A:Ensemble) : Ensemble := fun x:U => ~ In A x.
-  
+
   Definition Setminus (B C:Ensemble) : Ensemble :=
     fun x:U => In B x /\ ~ In C x.
-  
+
   Definition Subtract (B:Ensemble) (x:U) : Ensemble := Setminus B (Singleton x).
-  
+
   Inductive Disjoint (B C:Ensemble) : Prop :=
     Disjoint_intro : (forall x:U, ~ In (Intersection B C) x) -> Disjoint B C.
 
   Inductive Inhabited (B:Ensemble) : Prop :=
     Inhabited_intro : forall x:U, In B x -> Inhabited B.
-  
+
   Definition Strict_Included (B C:Ensemble) : Prop := Included B C /\ B <> C.
-  
+
   Definition Same_set (B C:Ensemble) : Prop := Included B C /\ Included C B.
-  
+
   (** Extensionality Axiom *)
 
   Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.