X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_sets.ma;h=1ca191339b697514c39b171ed9111ef8c6a1003c;hb=81b43e348e0c3e61114900d1e1df058ecc68cd90;hp=27b10aeefbac510bfc7d65a7d4ae70873a6483a0;hpb=603bbe202f09745133cefa4902f2b16fb17b70b8;p=helm.git

diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma
index 27b10aeef..1ca191339 100644
--- a/helm/software/matita/dama/ordered_sets.ma
+++ b/helm/software/matita/dama/ordered_sets.ma
@@ -692,4 +692,4 @@ qed.
 definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
 
 interpretation "Ordered set lt" 'lt a b =
- (cic:/matita/ordered_sets/lt.con _ _ a b).
+ (cic:/matita/ordered_sets/lt.con _ a b).