X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=5da934cdc8aa6661c76a4af35997b6fd49401713;hb=119da3f9ce130f7c4e8b23fcc491d221472ad657;hp=0a331f58b03164190e5eb2705941d5cce5e8d976;hpb=f336cc57864e1aebe9256240bf523fa5970d025a;p=helm.git

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 0a331f58b..5da934cdc 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -46,7 +46,7 @@
       <p>At the same time, proofs are an integrated part of the formalism, allowing, via the 
       <a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence">Curry Howard 
       isomorphism</a>, a smooth interplay between
-      specification and reasoning: proofs are objects of the language, and
+      specification, implementation and verification: proofs are objects of the language, and
       can be treated as normal data, naturally leading to a programming style
       akin to <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>, 
       where chunks of software 
@@ -58,6 +58,7 @@
       assembly of the kind traditionally used in embedded systems.
       </p>
       
+      <!--#include virtual="bottombar.shtml" -->
 
     </div>
   </body>