helm/www/matita/docs/manual/index.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
   3 <html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Matita V0.1.0
   4  Manual (rev. 0)</title><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0&#10; Manual (rev. 0)" /><link rel="next" href="sec_intro.html" title="Chapter 1. Introduction" /></head><body><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center"><span class="application">Matita</span> V0.1.0
   5  Manual (rev. 0)</th></tr><tr><td width="20%" align="left"> </td><th width="60%" align="center"> </th><td width="20%" align="right"> <a accesskey="n" href="sec_intro.html">Next</a></td></tr></table><hr /></div><div class="book" lang="en" xml:lang="en"><div class="titlepage"><div><div><h1 class="title"><a id="matita_manual"></a><span class="application">Matita</span> V0.1.0
   6  Manual (rev. 0)</h1></div><div><div class="authorgroup"><div class="author"><h3 class="author"><span class="firstname">Andrea</span> <span class="surname">Asperti</span></h3><div class="affiliation"><div class="address"><p> <code class="email">&lt;<a href="mailto:asperti@cs.unibo.it">asperti@cs.unibo.it</a>&gt;</code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Claudio</span> <span class="surname">Sacerdoti Coen</span></h3><div class="affiliation"><div class="address"><p> <code class="email">&lt;<a href="mailto:sacerdot@cs.unibo.it">sacerdot@cs.unibo.it</a>&gt;</code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Enrico</span> <span class="surname">Tassi</span></h3><div class="affiliation"><div class="address"><p> <code class="email">&lt;<a href="mailto:tassi@cs.unibo.it">tassi@cs.unibo.it</a>&gt;</code> </p></div></div></div><div class="author"><h3 class="author"><span class="firstname">Stefano</span> <span class="surname">Zacchiroli</span></h3><div class="affiliation"><div class="address"><p> <code class="email">&lt;<a href="mailto:zacchiro@cs.unibo.it">zacchiro@cs.unibo.it</a>&gt;</code> </p></div></div></div></div></div><div><p class="releaseinfo">This manual describes version 0.1.0
   7  of Matita.
   8     </p></div><div><p class="copyright">Copyright © 2006 The HELM team.</p></div><div><div class="legalnotice"><a id="id2472240"></a><p> This file is part of HELM, an Hypertextual, Electronic Library of
   9   Mathematics, developed at the Computer Science Department, University of
  10   Bologna, Italy.  </p><p> HELM is free software; you can redistribute it and/or modify it under
  11   the terms of the GNU General Public License as published by the Free
  12   Software Foundation; either version 2 of the License, or (at your option)
  13   any later version.  </p><p> HELM is distributed in the hope that it will be useful, but WITHOUT
  14   ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
  15   FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
  16   more details.  </p><p> You should have received a copy of the GNU General Public License
  17   along with HELM; if not, write to the Free Software Foundation, Inc., 59
  18   Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU
  19   General Public License is available at <a href="ghelp:gpl" target="_top">this link</a>. </p></div></div><div><div class="legalnotice"><a id="id2472567"></a><p class="legalnotice-title"><b>Feedback</b></p><p>To report a bug or make a suggestion regarding the <span class="application">Matita</span>
  20         application or this manual, follow the directions in the
  21         <a href="http://bugs.mowgli.cs.unibo.it" target="_top">HELM Bug
  22           Tracking System Page</a>.
  23       </p></div></div><div><div class="revhistory"><table border="1" width="100%" summary="Revision history"><tr><th align="left" valign="top" colspan="3"><b>Revision History</b></th></tr><tr><td align="left">Revision Matita V0.1.0
  24  Manual (rev. 0)</td><td align="left">February 2006</td><td> </td></tr><tr><td align="left" colspan="3">
  25           <p class="author">The HELM team
  26
  27           </p>
  28
  29         </td></tr><tr><td align="left">Revision 0</td><td align="left">4 February 2006</td><td align="left">HELM</td></tr><tr><td align="left" colspan="3">
  30    First draft completed.
  31    </td></tr></table></div></div></div><hr /></div><div class="toc"><p><b>Table of Contents</b></p><dl><dt><span class="chapter"><a href="sec_intro.html">1. Introduction</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_intro.html#Features">Features</a></span></dt><dt><span class="sect1"><a href="WrtCoq.html">Matita vs Coq</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_install.html">2. Installation</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_install.html#inst_from_src">Installing from sources</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_install.html#get_source_code">Getting the source code</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_requirements">Requirements</a></span></dt><dt><span class="sect2"><a href="sec_install.html#database_setup">Database setup</a></span></dt><dt><span class="sect2"><a href="sec_install.html#build_instructions">Compiling and installing</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_gettingstarted.html">3. Getting started</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_gettingstarted.html#unicode">How to type Unicode symbols</a></span></dt><dt><span class="sect1"><a href="cicbrowser.html">Browsing and searching</a></span></dt><dd><dl><dt><span class="sect2"><a href="cicbrowser.html#browsinglib">Browsing the library</a></span></dt><dt><span class="sect2"><a href="cicbrowser.html#aboutproof">Looking at a proof under development</a></span></dt><dt><span class="sect2"><a href="cicbrowser.html#whelp">Searching the library</a></span></dt></dl></dd><dt><span class="sect1"><a href="authoring.html">Authoring</a></span></dt><dd><dl><dt><span class="sect2"><a href="authoring.html#developments">How to use developments</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_terms.html">4. Syntax</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_terms.html#terms_and_co">Terms &amp; co.</a></span></dt><dd><dl><dt><span class="sect2"><a href="sec_terms.html#lexical">Lexical conventions</a></span></dt><dt><span class="sect2"><a href="sec_terms.html#terms">Terms</a></span></dt></dl></dd><dt><span class="sect1"><a href="axiom_definition_declaration.html">Definitions and declarations</a></span></dt><dd><dl><dt><span class="sect2"><a href="axiom_definition_declaration.html#axiom">axiom</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#definition">definition</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#inductive">(co)inductive types declaration</a></span></dt><dt><span class="sect2"><a href="axiom_definition_declaration.html#record">record</a></span></dt></dl></dd><dt><span class="sect1"><a href="proofs.html">Proofs</a></span></dt><dd><dl><dt><span class="sect2"><a href="proofs.html#theorem">theorem</a></span></dt><dt><span class="sect2"><a href="proofs.html#variant">variant</a></span></dt><dt><span class="sect2"><a href="proofs.html#lemma">lemma</a></span></dt><dt><span class="sect2"><a href="proofs.html#fact">fact</a></span></dt><dt><span class="sect2"><a href="proofs.html#remark">remark</a></span></dt></dl></dd></dl></dd><dt><span class="chapter"><a href="sec_usernotation.html">5. Extending the syntax</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_usernotation.html#id2526491">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tactics.html">6. Tactics</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tactics.html#tac_absurd">absurd</a></span></dt><dt><span class="sect1"><a href="tac_apply.html">apply</a></span></dt><dt><span class="sect1"><a href="tac_assumption.html">assumption</a></span></dt><dt><span class="sect1"><a href="tac_auto.html">auto</a></span></dt><dt><span class="sect1"><a href="tac_clear.html">clear</a></span></dt><dt><span class="sect1"><a href="tac_clearbody.html">clearbody</a></span></dt><dt><span class="sect1"><a href="tac_change.html">change</a></span></dt><dt><span class="sect1"><a href="tac_constructor.html">constructor</a></span></dt><dt><span class="sect1"><a href="tac_contradiction.html">contradiction</a></span></dt><dt><span class="sect1"><a href="tac_cut.html">cut</a></span></dt><dt><span class="sect1"><a href="tac_decompose.html">decompose</a></span></dt><dt><span class="sect1"><a href="tac_discriminate.html">discriminate</a></span></dt><dt><span class="sect1"><a href="tac_elim.html">elim</a></span></dt><dt><span class="sect1"><a href="tac_elimType.html">elimType</a></span></dt><dt><span class="sect1"><a href="tac_exact.html">exact</a></span></dt><dt><span class="sect1"><a href="tac_exists.html">exists</a></span></dt><dt><span class="sect1"><a href="tac_fail.html">failt</a></span></dt><dt><span class="sect1"><a href="tac_fold.html">fold</a></span></dt><dt><span class="sect1"><a href="tac_fourier.html">fourier</a></span></dt><dt><span class="sect1"><a href="tac_fwd.html">fwd</a></span></dt><dt><span class="sect1"><a href="tac_generalize.html">generalize</a></span></dt><dt><span class="sect1"><a href="tac_id.html">id</a></span></dt><dt><span class="sect1"><a href="tac_injection.html">injection</a></span></dt><dt><span class="sect1"><a href="tac_intro.html">intro</a></span></dt><dt><span class="sect1"><a href="tac_intros.html">intros</a></span></dt><dt><span class="sect1"><a href="tac_inversion.html">inversion</a></span></dt><dt><span class="sect1"><a href="tac_lapply.html">lapply</a></span></dt><dt><span class="sect1"><a href="tac_left.html">left</a></span></dt><dt><span class="sect1"><a href="tac_letin.html">letin</a></span></dt><dt><span class="sect1"><a href="tac_normalize.html">normalize</a></span></dt><dt><span class="sect1"><a href="tac_paramodulation.html">paramodulation</a></span></dt><dt><span class="sect1"><a href="tac_reduce.html">reduce</a></span></dt><dt><span class="sect1"><a href="tac_reflexivity.html">reflexivity</a></span></dt><dt><span class="sect1"><a href="tac_replace.html">change</a></span></dt><dt><span class="sect1"><a href="tac_rewrite.html">rewrite</a></span></dt><dt><span class="sect1"><a href="tac_right.html">right</a></span></dt><dt><span class="sect1"><a href="tac_ring.html">ring</a></span></dt><dt><span class="sect1"><a href="tac_simplify.html">simplify</a></span></dt><dt><span class="sect1"><a href="tac_split.html">split</a></span></dt><dt><span class="sect1"><a href="tac_symmetry.html">symmetry</a></span></dt><dt><span class="sect1"><a href="tac_transitivity.html">transitivity</a></span></dt><dt><span class="sect1"><a href="tac_unfold.html">unfold</a></span></dt><dt><span class="sect1"><a href="tac_whd.html">whd</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_tacticals.html">7. Tacticals</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_tacticals.html#id2534769">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_commands.html">8. Other commands</a></span></dt><dd><dl><dt><span class="sect1"><a href="sec_commands.html#id2535309">Introduction</a></span></dt></dl></dd><dt><span class="chapter"><a href="sec_license.html">9. License</a></span></dt></dl></div><div class="list-of-figures"><p><b>List of Figures</b></p><dl><dt>3.1. <a href="authoring.html#id2520494">The Developments window</a></dt></dl></div><div class="list-of-tables"><p><b>List of Tables</b></p><dl><dt>2.1. <a href="sec_install.html#id2518871"> <span class="application">configure</span> command line
  32             arguments</a></dt><dt>4.1. <a href="sec_terms.html#id2521399">id</a></dt><dt>4.2. <a href="sec_terms.html#id2521488">nat</a></dt><dt>4.3. <a href="sec_terms.html#id2521498">uri</a></dt><dt>4.4. <a href="sec_terms.html#id2521554">Terms</a></dt><dt>4.5. <a href="sec_terms.html#id2522106">Simple terms</a></dt><dt>4.6. <a href="sec_terms.html#id2522561">Arguments</a></dt><dt>4.7. <a href="sec_terms.html#id2522763">Miscellaneous arguments</a></dt><dt>4.8. <a href="sec_terms.html#id2522867">Pattern matching</a></dt></dl></div></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"> </td><td width="20%" align="center"> </td><td width="40%" align="right"> <a accesskey="n" href="sec_intro.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top"> </td><td width="20%" align="center"> </td><td width="40%" align="right" valign="top"> Chapter 1. Introduction</td></tr></table></div></body></html>