X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fminimization.ma;h=2959d0f3d1d14eb4b919dff3903d877f7047ce84;hb=a5c551d0b7399f00e8eef3dfb06e2a0895eac3d4;hp=eda9d016618d1031be5b126b65b35ca105b9ee11;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/arithmetics/minimization.ma b/weblib/arithmetics/minimization.ma
index eda9d0166..2959d0f3d 100644
--- a/weblib/arithmetics/minimization.ma
+++ b/weblib/arithmetics/minimization.ma
@@ -23,7 +23,7 @@ let rec max' i f d ≝
       
 definition max ≝ λn.λf.max' n f O.
 
-theorem max_O: ∀f. max O f = O.
+theorem max_O: ∀f. A href="cic:/matita/arithmetics/minimization/max.def(2)"max/A O f = O.
 // qed.
 
 theorem max_cases: ∀f.∀n.