From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 25 Nov 2007 14:22:16 +0000 (+0000)
Subject: commented out things that DO NOT compile
X-Git-Tag: 0.4.98~1
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c52605b5b949f2ceafbe788c8f7bf7e74dc89b5c;p=helm.git

commented out things that DO NOT compile
---

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
+*)