X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fsupremum.ma;h=2ce417ecce9398a7e9405ce347ae65ff15772718;hb=943c8baae10afee070468ab54f4bf86563df2418;hp=be8495970a737e9f926066f381c134b7a9784dd0;hpb=c5a4db6c1020488d0792cee00dcf395a0ce54735;p=helm.git

diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma
index be8495970..2ce417ecc 100644
--- a/helm/software/matita/library/dama/supremum.ma
+++ b/helm/software/matita/library/dama/supremum.ma
@@ -121,7 +121,7 @@ interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l
 interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
 
 lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
+ Type_OF_ordered_set nat_ordered_set →
    hos_carr (os_l (nat_ordered_set)).
 intros; assumption;
 qed.