From f336cc57864e1aebe9256240bf523fa5970d025a Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 3 Apr 2012 10:37:54 +0000
Subject: [PATCH 1/1] modifiche

---
 helm/www/matita/matita.shtml    |  9 +--------
 helm/www/matita/matita_it.shtml | 10 +++++++++-
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index b06da9bd0..0a331f58b 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -28,13 +28,6 @@
       <p>
       </p>
 <!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
-
-      <p class="spaced">
-      <span class="screenshots">
-	<a class="quiet" href="images/screenshot-matita.png">
-	  <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
-	</a>
-      </span>
       
       <p>An interactive prover is a software tool aiding the development of 
       formal proofs by man-machine collaboration. It provides a formal language 
@@ -60,7 +53,7 @@
       come equipped with proofs of (some of) their properties.</p>
 
       <p>Matita is currently adopted in the European Union "Certified Complexity" Project
-      <a href="http://cerco.cs.unibo.it/">CerCo<a> for the formal verification of a 
+      <a href="http://cerco.cs.unibo.it/">CerCo</a> for the formal verification of a 
       complexity-preserving compiler from a large subset of C to a microcontroller 
       assembly of the kind traditionally used in embedded systems.
       </p>
diff --git a/helm/www/matita/matita_it.shtml b/helm/www/matita/matita_it.shtml
index 49db3b9f6..8235b013a 100644
--- a/helm/www/matita/matita_it.shtml
+++ b/helm/www/matita/matita_it.shtml
@@ -26,6 +26,14 @@
       <a href="http://www.unibo.it">Universita' degli Studi di Bologna</a>.
       </p>
 
+      <p>Un dimostratore interattivo e' uno strumento software di 
+     ausilio alla dimostrazione formale di teoremi attraverso 
+     la collaborazione tra l'uomo e la macchina. Fornisce un liguaggio
+     formale in cui coesistono definizioni matematiche, algoritmi eseguibili, 
+     teoremi e relative dimostrazioni, ed un ambiente interattivo che tiene
+     traccia dello stato corrente delle prove, e le aggiorna in funzione dei
+     comandi (tattiche) impartiti dall'utente. </p>
+
       <p>
       Matita si fonda su di un Sistema di <a href="http://en.wikipedia.org/wiki/Dependent_type">Tipi Dipendenti</a> noto con il nome di Calcolo delle
       Costruzioni Induttive.</p>
@@ -44,7 +52,7 @@
       <a href="http://en.wikipedia.org/wiki/Proof-carrying_code">proof-carrying-code</a>, dove frammenti di software sono arricchiti con dimostrazioni di
       alcune delle loro proprieta'.</p>
 
-      <p>Matita e' attualmente adottato nel Progetto Europeo <a href="http://cerco.cs.unibo.it/">CerCo<a> (Certified Complexity)  per la verifica formale
+      <p>Matita e' attualmente adottato nel Progetto Europeo <a href="http://cerco.cs.unibo.it/">CerCo</a> (Certified Complexity)  per la verifica formale
       della preservazione della complessita' durante la fase di compilazione
       da linguaggio C verso un linguaggio assembly tipico di microprocessori
       per sistemi embedded.</p>
-- 
2.39.2