X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_sets.ma;h=9cd9f58a93e0db8b538b2ca3e17b430bed66def2;hb=c4050b216986232e7ad0095542b940960626614b;hp=a7f772f34a5b90ec4a59bd1158d2d17660dfbb1a;hpb=3a68c1b1f891a19d87c9963a5da2e4b76aadf455;p=helm.git

diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma
index a7f772f34..9cd9f58a9 100644
--- a/helm/software/matita/dama/ordered_sets.ma
+++ b/helm/software/matita/dama/ordered_sets.ma
@@ -132,6 +132,8 @@ cases E (T f cRf cTf); simplify;
 |2: intros (x y z); apply Or_symmetric; apply cTf; assumption;]
 qed. 
 
+(*
+
 definition reverse_pordered_set: pordered_set → pordered_set.
 intros (p); apply (mk_pordered_set (reverse_excedence p));
 generalize in match (reverse_excedence p); intros (E); cases E (T f cRf cTf);
@@ -212,6 +214,8 @@ record cotransitively_ordered_set: Type :=
  }.
 *)
 
+*)
+
 definition total_order_property : ∀E:excedence. Type ≝
   λE:excedence. ∀a,b:E. a ≰ b → a < b.