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
49 <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&path=%2Ftrunk%2Fhelm%2Fsoftware%2Fmatita%2Fhelp%2FC%2F&rev=0&sc=0">matita/help/C/</a> folder. </p>
51 <h2>Tutorials<a name="tutorial"></a></h2>
53 <p>A not so short <a href="FILES/matita-tut.pdf">tutorial</a> by
54 A.Asperti, discussing some basic notions of number theory, for
55 the stable version of Matita.</p>
57 <p>A <a href="docs/tutorial/igft.html">tutorial</a> by E.Tassi based on
58 the formalization of the paper "Between formal topology and game theory:
59 an explicit solution for the conditions for an inductive generation of
60 formal topologies" by S.Berardi and S.Valentini. The tutorial describes
61 the ng version of Matita (not officially released yet, cohexisting with
62 the stable system in version 0.5.8). If some characters are not displayed
63 correctly (i.e. you are not using firefox) you may try the
64 <a href="docs/tutorial/igft.pdf">pdf version</a>.
68 <h2>Exercises<a name="exercises"></a></h2>
70 <p>Some commented <a href="FILES/matita-ex.pdf">exercises</a> given at the
71 <a href="http://typessummerschool07.cs.unibo.it">types summer school 2007</a>
72 by C.Sacerdoti and E.Tassi.
76 <!--#include virtual="papers.shtml" -->
78 <h2>Large Developments</h2>
79 <!--#include virtual="theses.shtml" -->
81 <!--#include virtual="bottombar.shtml" -->