X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fexp.ma;h=6fcd9da0ec646620f36b8546af0d54f1854dad2c;hb=be797cb755104e7c8709f2602ced5c46c5c1987b;hp=c0d36377305f9f1878cb16f419f27294ed72358f;hpb=7bbce6bc163892cfd99cfcda65db42001b86789f;p=helm.git

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index c0d363773..6fcd9da0e 100644
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -37,7 +37,7 @@ theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
 intro.simplify.rewrite < times_n_SO.reflexivity.
 qed.
 
-theorem bad : \forall n,p,q:nat. 
+theorem exp_exp_times : \forall n,p,q:nat. 
 eq nat (exp (exp n p) q) (exp n (times p q)).
 intros.
 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.