commented out things that DO NOT compile

[helm.git] / matita / library / nat / chebyshev.ma

diff --git a/matita/library/nat/chebyshev.ma b/matita/library/nat/chebyshev.ma
index c06675d0e2d3db98e1019496b3ed94887609fba5..f7ffbf0460eb08cce593f98083167abe7f39b1dc 100644 (file)
--- a/matita/library/nat/chebyshev.ma
+++ b/matita/library/nat/chebyshev.ma
@@ -1199,6 +1199,8 @@ apply (trans_le ? (B((S(S O))*n)*A n))
   ]
 qed.
 
+(*
+
 (* da spostare *)
 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
 intros.elim p
@@ -1707,4 +1709,4 @@ elim (lt_O_to_or_eq_S m)
        
        a*log a-a+k*log a
        
-*)
\ No newline at end of file
+*)