X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=33a658479329d10443f9b17d9aa528966ef74b08;hb=b9ee81d329f267b12d05c05cbd3509b27d3d55a0;hp=57298c377974123e06b9e4ba7e40e57310a992ab;hpb=d0b2bceffedce633f496b4e4fcc557be73fbfe1d;p=helm.git

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 57298c377..33a658479 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -14,31 +14,35 @@
 	<img src="images/matita-text-big.png" alt="Big Matita label" />
       </div>
 
-      <p> Matita is a new document-centric interactive theorem prover that
-      integrates several <a href="http://www.mkm-ig.org">Mathematical Knowledge
-	Management</a> tools and techniques. </p>
+      <p class="spaced">
+      Matita (that means <em>pencil</em> in italian) is an experimental, 
+	interactive theorem prover under development at the 
+      <a href="http://www.cs.unibo.it">Computer Science Department</a> of the 
+      <a href="http://www.unibo.it">University of Bologna</a>.
+      </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>
-      Matita is <strong>traditional</strong>. Its logical foundation is the
-      Calculus of (Co)Inductive Constructions (CIC). It can re-use
-      mathematical concepts produced by other proof assistants like
-      <a href="http://coq.inria.fr">Coq</a> and encoded in an
-      <a href="http://www.w3.org/XML/">XML</a> encoding of CIC. The interaction
-      paradigm of Matita is familiar, being inspired by CtCoq and
-      <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>. Its
-      proof language is procedural in the same spirit of LCF. </p>
-
-      <p> Matita is <strong>innovative</strong>: </p>
-      <ul>
-
-	<li>
-	<p>
-	<span class="screenshots">
+      
+      Matita is based on the 
+      Calculus of (Co)Inductive Constructions, and is compatible, at some
+      extent, with <a href="http://coq.inria.fr">Coq</a>.
+      It is a reasonably small and simple application, whose 
+      architectural and software complexity is meant to be mastered by 
+      students, providing a tool particularly suited for testing innovative 
+      ideas and solutions.
+      Matita adopts a tactic based editing mode; (XML-encoded) proof objects
+      are produced for storage and exchange. 
+      </p>
+      
+      <p class="spaced"> 
+      <span class="screenshots">
 	  <a class="quiet" href="images/screenshot-matita-href.png">
 	    <img src="images/MINI_screenshot-matita-href.png" alt="Matita screenshot: hyperlinks" />
 	  </a>
@@ -46,16 +50,14 @@
 	    <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
 	  </a>
 	</span>
-	the user interface sports high quality bidimensional rendering of
-	proofs and formulae transformed on-the-fly to <a
-	  href="http://www.w3.org/Math/">MathML</a> markup, on which direct
-	manipulation of the underlying CIC terms is still possible;
-	</p>
-	</li>
+      The graphical interface has been inspired by CtCoq and
+      <a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a>.
+      It supports high quality bidimensional rendering of
+      proofs and formulae transformed on-the-fly to 
+      <a href="http://www.w3.org/Math/">MathML</a> markup</p>
 
-	<li>
-	<p>
-	<span class="screenshots">
+      <p class="spaced">
+      <span class="screenshots">
 	  <a class="quiet" href="images/screenshot-cicbrowser-browsing.png">
 	    <img src="images/MINI_screenshot-cicbrowser-browsing.png" alt="Matita screenshot: library browsing" />
 	  </a>
@@ -64,31 +66,26 @@
 	  </a>
 	  <!--
 	  <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
-	    <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering" />
+	    <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
 	  </a>
 	  -->
-	</span>
-	the knowledge base is distributed: every authored concepts can be
-	published becoming part of the Matita library which can be <a
-	  href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
-	(locally or on the World Wide Web) and <a
-	  href="http://helm.cs.unibo.it/whelp/"> searched by means of
-	  content-based queries</a>; </p>
-	</li>
+      </span>
+      
+      The knowledge base can be 
+      <a href="http://helm.cs.unibo.it/browse/">browsed as an hypertext</a>
+      (locally or on the World Wide Web) and 
+      <a href="http://helm.cs.unibo.it/whelp/"> searched by means of
+      content-based queries</a>; </p>
 
-	<li>
-	<p>
+      <p class="spaced">
 	<span class="screenshots">
 	  <a class="quiet" href="images/screenshot-tinycals.png">
 	    <img src="images/MINI_screenshot-tinycals.png" alt="Matita screenshot: tinycals" />
 	  </a>
 	</span>
-	the tactical language, part of the proof language, has
+	The tactical language, part of the proof language, has
 	step-by-step semantics, enabling inspection and replaying of deeply
 	structured proof scripts. </p>
-	</li>
-
-      </ul>
 
       <!--#include virtual="bottombar.shtml" -->
     </div>