From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 3 Apr 2012 08:35:11 +0000 (+0000)
Subject: prova
X-Git-Tag: make_still_working~1828
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0692f9fb99211c02a93c72d58c9177f9f994e4d9;p=helm.git

prova
---

diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml
index 4c9e166c5..a68b48830 100644
--- a/helm/www/matita/matita.shtml
+++ b/helm/www/matita/matita.shtml
@@ -11,13 +11,6 @@
     <!--#include virtual="news.shtml" -->
     <div class="main">
 
-      <div class="topimage">
-	<img src="images/matita-text-big.png" alt="Matita" />
-	<a href="matita_it.shtml">
-         <img src="flags/wit.gif" alt="italian flag" />
-        </a>
-      </div>
-
       <p class="spaced">
       Matita (that means <em>pencil</em> in italian) is an experimental, 
 	interactive theorem prover under development at the 
@@ -27,79 +20,7 @@
 
 <!-- <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 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>
-	  <a class="quiet" href="images/screenshot-matita-selection.png">
-	    <img src="images/MINI_screenshot-matita-selection.png" alt="Matita screenshot: direct manipulation" />
-	  </a>
-	</span>
-      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>
-
-      <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>
-	  <a class="quiet" href="images/screenshot-cicbrowser-query.png">
-	    <img src="images/MINI_screenshot-cicbrowser-query.png" alt="Matita screenshot: Whelp query" />
-	  </a>
-	  <!--
-	  <a class="quiet" href="images/screenshot-cicbrowser-proof.png">
-	    <img src="images/MINI_screenshot-cicbrowser-proof.png" alt="Matita screenshot: proof rendering"
-	  </a>
-	  -->
-      </span>
-      
-      The <a href="library.shtml">knowledge base</a> 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>
-
-      <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
-	step-by-step semantics, enabling inspection and replaying of deeply
-	structured proof scripts. </p>
-        
-      <p>Matita is partially supported by the following Projects: </p>
-      <ul>
-        <li><a href="http://www.cs.chalmers.se/Cs/Research/Logic/Types/">
-          Types Project</a></li>
-       <li><a href="http://www.mctafi.math.unipd.it/">McTafi</a></li>
-       <li><a href="http://dama.cs.unibo.it/">Dama</a></li>
-      </ul>
 
-      <!--#include virtual="bottombar.shtml" -->
     </div>
   </body>
 </html>