From c52605b5b949f2ceafbe788c8f7bf7e74dc89b5c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 25 Nov 2007 14:22:16 +0000
Subject: [PATCH] commented out things that DO NOT compile

---
 matita/library/nat/chebyshev.ma | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/matita/library/nat/chebyshev.ma b/matita/library/nat/chebyshev.ma
index c06675d0e..f7ffbf046 100644
--- 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
+*)
-- 
2.39.2