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  User Manual (rev. 1α)</title><link rel="stylesheet" href="docbook.css" type="text/css" /><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0&#10; User Manual (rev. 1α)" /><link rel="next" href="sec_intro.html" title="Chapter 1. Introduction" /></head><body><a xmlns="" href="../../"><div class="matita_logo"><img src="../../images/matita-tiny.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center"><span class="application">Matita</span> V0.1.0
   5  User Manual (rev. 1α)</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  User Manual (rev. 1α)</h1></div><div><ul xmlns="" class="authorgroup"><li class="author">Andrea Asperti &lt;<a href="mailto:asperti@cs.unibo.it">asperti@cs.unibo.it</a>&gt;</li><li class="author">Claudio Sacerdoti Coen &lt;<a href="mailto:sacerdot@cs.unibo.it">sacerdot@cs.unibo.it</a>&gt;</li><li class="author">Enrico Tassi &lt;<a href="mailto:tassi@cs.unibo.it">tassi@cs.unibo.it</a>&gt;</li><li class="author">Stefano Zacchiroli &lt;<a href="mailto:zacchiro@cs.unibo.it">zacchiro@cs.unibo.it</a>&gt;</li></ul></div><div><p class="copyright">Copyright © 2006 The HELM team.</p></div><div><div class="legalnotice"><a id="id2509491"></a><p> Both Matita and this document are free software, you can
   7         redistribute them and/or modify them under the terms of the GNU General
   8         Public License as published by the Free Software Foundation.  See <a href="sec_license.html" title="Chapter 9. License">Chapter 9, <i>License</i></a> for more information. </p></div></div><div><div xmlns="" class="revhistory"><span class="revision">Revision: <span class="revnumber">1α</span>, <span class="date">10/06/2006</span></span></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#id2527183">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#id2535462">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#id2536001">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#id2521185">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#id2519563"> <span class="application">configure</span> command line
   9             arguments</a></dt><dt>4.1. <a href="sec_terms.html#id2522091">id</a></dt><dt>4.2. <a href="sec_terms.html#id2522119">nat</a></dt><dt>4.3. <a href="sec_terms.html#id2522189">uri</a></dt><dt>4.4. <a href="sec_terms.html#id2522245">Terms</a></dt><dt>4.5. <a href="sec_terms.html#id2522798">Simple terms</a></dt><dt>4.6. <a href="sec_terms.html#id2523252">Arguments</a></dt><dt>4.7. <a href="sec_terms.html#id2523455">Miscellaneous arguments</a></dt><dt>4.8. <a href="sec_terms.html#id2523559">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>