1 <!--#include virtual="xhtml-header.shtml" -->
3 <html xmlns="http://www.w3.org/1999/xhtml">
5 <title>Matita - Documentation</title>
6 <!--#include virtual="xhtml-meta.shtml" -->
7 <script type="text/javascript">
8 function toggleAbstracts() {
9 abstracts = document.getElementsByTagName("span");
10 len = abstracts.length;
11 for (i=0; i != len-1; i++) {
12 elt = abstracts.item(i);
13 if (elt.hasAttribute("class")) {
14 if (elt.getAttribute("class") == "paper_abstract") {
15 if (elt.style.display != "none") {
16 elt.style.display = "none";
18 elt.style.display = "inline";
27 <!--#include virtual="menubar.shtml" -->
29 <h1>Matita Documentation</h1>
31 <h2>User Manual<a name="manual"></a></h2>
33 <p> The Matita User Manual is accessible from Matita itself via the
34 <a href="http://developer.gnome.org/arch/doc/help.html">GNOME Help
35 System</a>, just hit <kbd><F1></kbd> while running Matita and it
36 will be shown to you. </p>
38 <p> Alternatively you can browse it in
39 <!--<a href="http://www.w3.org/TR/xhtml1/">-->XHTML<!--</a>--> format:
42 <li> <a href="docs/manual/html">Matita User Manual (XHTML format, multiple pages)</a>
46 <p> The source code of the user manual (in <a
47 href="http://www.oasis-open.org/docbook/">DocBook</a> format) is
48 available from our repository, in the
50 href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fmatita%2Fmatita%2Fhelp%2FC%2F&#a984ecdd087e75087ba2f4b21276224c4">matita/help/C/</a> folder. </p>
52 <!-- XXX: OUTDATED (WR)
54 <h2>Tutorials<a name="tutorial"></a></h2>
56 <p>A not so short <a href="FILES/matita-tut.pdf">tutorial</a> by
57 A.Asperti, discussing some basic notions of number theory, for
58 the stable version of Matita.</p>
60 <p>A <a href="docs/tutorial/igft.html">tutorial</a> by E.Tassi based on
61 the formalization of the paper "Between formal topology and game theory:
62 an explicit solution for the conditions for an inductive generation of
63 formal topologies" by S.Berardi and S.Valentini. The tutorial describes
64 the ng version of Matita (not officially released yet, cohexisting with
65 the stable system in version 0.5.8). If some characters are not displayed
66 correctly (i.e. you are not using firefox) you may try the
67 <a href="docs/tutorial/igft.pdf">pdf version</a>.
71 <h2>Exercises<a name="exercises"></a></h2>
73 <p>Some commented <a href="FILES/matita-ex.pdf">exercises</a> given at the
74 <a href="http://typessummerschool07.cs.unibo.it">types summer school 2007</a>
75 by C.Sacerdoti and E.Tassi.
80 <!--#include virtual="papers.shtml" -->
82 <!-- XXX: OUTDATED (WR)
83 <h2>Large Developments</h2>
84 include virtual="theses.shtml"
87 <!--#include virtual="bottombar.shtml" -->