X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fsupremum.ma;h=2ce417ecce9398a7e9405ce347ae65ff15772718;hb=8d961585c4ff785d558d5b4c84adf656595ca487;hp=be8495970a737e9f926066f381c134b7a9784dd0;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;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.