]> matita.cs.unibo.it Git - helm.git/commitdiff
removed a comment/bug report about let..in rendering, now fixed
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 13 Sep 2005 14:11:45 +0000 (14:11 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 13 Sep 2005 14:11:45 +0000 (14:11 +0000)
helm/matita/library/nat/primes.ma

index dddd9151657ed3b28764fa3a543fcacfcc648193..500c8117f70355c181e55924eaa3befbecd23279 100644 (file)
@@ -567,7 +567,6 @@ apply nat_case n.
 change with prime (S(S O)).
 apply primeb_to_Prop (S(S O)).
 intro.
-(* ammirare la resa del letin !! *)
 change with
 let previous_prime \def (nth_prime m) in
 let upper_bound \def S (fact previous_prime) in