]> matita.cs.unibo.it Git - helm.git/commitdiff
reshaped manual
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 7 Feb 2006 13:39:52 +0000 (13:39 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 7 Feb 2006 13:39:52 +0000 (13:39 +0000)
helm/software/configure.ac
helm/software/matita/dist/version.txt.in [new file with mode: 0644]
helm/software/matita/help/C/intro.xml [new file with mode: 0644]
helm/software/matita/help/C/legal.xml
helm/software/matita/help/C/matita.xml
helm/software/matita/help/C/tactics.xml [new file with mode: 0644]
helm/software/matita/help/C/terms.xml [new file with mode: 0644]

index 15470ef37cd8102dccbb74d84f68d8f007352e73..afb09d8053514a0ad1fe598c4e3bf54756bb1bfb 100644 (file)
@@ -154,19 +154,19 @@ AC_ARG_WITH(dbhost,
 AC_MSG_RESULT($DBHOST)
 
 AC_SUBST(CAMLP4O)
-AC_SUBST(DISTRIBUTED)
 AC_SUBST(DBHOST)
 AC_SUBST(DEBUG)
-AC_SUBST(TRANSFORMER_MODULE)
-AC_SUBST(FINDLIB_REQUIRES)
+AC_SUBST(DISTRIBUTED)
 AC_SUBST(FINDLIB_CREQUIRES)
+AC_SUBST(FINDLIB_REQUIRES)
 AC_SUBST(HAVE_OCAMLOPT)
 AC_SUBST(LABLGLADECC)
+AC_SUBST(MATITA_VERSION)
 AC_SUBST(OCAMLFIND)
 AC_SUBST(OCAMLPATH)
 AC_SUBST(RT_BASE_DIR)
 AC_SUBST(SRCROOT)
-AC_SUBST(MATITA_VERSION)
+AC_SUBST(TRANSFORMER_MODULE)
 
 AC_OUTPUT([
   components/extlib/componentsConf.ml
@@ -175,5 +175,6 @@ AC_OUTPUT([
   matita/matita.conf.xml.build
   matita/buildTimeConf.ml
   matita/gtkmathview.matita.conf.xml
+  matita/dist/version.txt
   Makefile.defs
 ])
diff --git a/helm/software/matita/dist/version.txt.in b/helm/software/matita/dist/version.txt.in
new file mode 100644 (file)
index 0000000..c275a8c
--- /dev/null
@@ -0,0 +1 @@
+@MATITA_VERSION@
diff --git a/helm/software/matita/help/C/intro.xml b/helm/software/matita/help/C/intro.xml
new file mode 100644 (file)
index 0000000..5510c8e
--- /dev/null
@@ -0,0 +1,15 @@
+
+<!-- ============= Introduction ============================== -->
+
+<sect1 id="sec_intro">
+  <title>Introduction</title>
+  <sect2 id="what">
+    <title>What is Matita?</title>
+
+    <para>
+      <application>Matita</application> is a proof assistant for ...
+    </para>
+
+  </sect2>
+</sect1>
+
index ac97e1de4d6b09dfc51dbe5a6366c33de5a5b456..d457ff463ec66c0833c6102ea4392f6a9c69c6e7 100644 (file)
@@ -1,76 +1,19 @@
-  <legalnotice id="legalnotice">
-       <para>
-         Permission is granted to copy, distribute and/or modify this
-         document under the terms of the GNU Free Documentation
-         License (GFDL), Version 1.1 or any later version published
-         by the Free Software Foundation with no Invariant Sections,
-         no Front-Cover Texts, and no Back-Cover Texts.  You can find
-         a copy of the GFDL at this <ulink type="help"
-         url="ghelp:fdl">link</ulink> or in the file COPYING-DOCS
-         distributed with this manual.
-         </para>
-         <para> This manual is part of a collection of GNOME manuals
-          distributed under the GFDL.  If you want to distribute this
-          manual separately from the collection, you can do so by
-          adding a copy of the license to the manual, as described in
-          section 6 of the license.
-       </para>
+<para> This file is part of HELM, an Hypertextual, Electronic Library of
+  Mathematics, developed at the Computer Science Department, University of
+  Bologna, Italy.  </para>
 
-       <para>
-         Many of the names used by companies to distinguish their
-         products and services are claimed as trademarks. Where those
-         names appear in any GNOME documentation, and the members of
-         the GNOME Documentation Project are made aware of those
-         trademarks, then the names are in capital letters or initial
-         capital letters.
-       </para>
+<para> HELM is free software; you can redistribute it and/or modify it under
+  the terms of the GNU General Public License as published by the Free
+  Software Foundation; either version 2 of the License, or (at your option)
+  any later version.  </para>
 
-       <para>
-         DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT ARE PROVIDED
-         UNDER  THE TERMS OF THE GNU FREE DOCUMENTATION LICENSE
-         WITH THE FURTHER UNDERSTANDING THAT:
-
-         <orderedlist>
-               <listitem>
-                 <para>DOCUMENT IS PROVIDED ON AN "AS IS" BASIS,
-                    WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR
-                    IMPLIED, INCLUDING, WITHOUT LIMITATION, WARRANTIES
-                    THAT THE DOCUMENT OR MODIFIED VERSION OF THE
-                    DOCUMENT IS FREE OF DEFECTS MERCHANTABLE, FIT FOR
-                    A PARTICULAR PURPOSE OR NON-INFRINGING. THE ENTIRE
-                    RISK AS TO THE QUALITY, ACCURACY, AND PERFORMANCE
-                    OF THE DOCUMENT OR MODIFIED VERSION OF THE
-                    DOCUMENT IS WITH YOU. SHOULD ANY DOCUMENT OR
-                    MODIFIED VERSION PROVE DEFECTIVE IN ANY RESPECT,
-                    YOU (NOT THE INITIAL WRITER, AUTHOR OR ANY
-                    CONTRIBUTOR) ASSUME THE COST OF ANY NECESSARY
-                    SERVICING, REPAIR OR CORRECTION. THIS DISCLAIMER
-                    OF WARRANTY CONSTITUTES AN ESSENTIAL PART OF THIS
-                    LICENSE. NO USE OF ANY DOCUMENT OR MODIFIED
-                    VERSION OF THE DOCUMENT IS AUTHORIZED HEREUNDER
-                    EXCEPT UNDER THIS DISCLAIMER; AND
-                 </para>
-               </listitem>
-               <listitem>
-                 <para>UNDER NO CIRCUMSTANCES AND UNDER NO LEGAL
-                       THEORY, WHETHER IN TORT (INCLUDING NEGLIGENCE),
-                       CONTRACT, OR OTHERWISE, SHALL THE AUTHOR,
-                       INITIAL WRITER, ANY CONTRIBUTOR, OR ANY
-                       DISTRIBUTOR OF THE DOCUMENT OR MODIFIED VERSION
-                       OF THE DOCUMENT, OR ANY SUPPLIER OF ANY OF SUCH
-                       PARTIES, BE LIABLE TO ANY PERSON FOR ANY
-                       DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR
-                       CONSEQUENTIAL DAMAGES OF ANY CHARACTER
-                       INCLUDING, WITHOUT LIMITATION, DAMAGES FOR LOSS
-                       OF GOODWILL, WORK STOPPAGE, COMPUTER FAILURE OR
-                       MALFUNCTION, OR ANY AND ALL OTHER DAMAGES OR
-                       LOSSES ARISING OUT OF OR RELATING TO USE OF THE
-                       DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT,
-                       EVEN IF SUCH PARTY SHALL HAVE BEEN INFORMED OF
-                       THE POSSIBILITY OF SUCH DAMAGES.
-                 </para>
-               </listitem>
-         </orderedlist>
-       </para>
-  </legalnotice>
+<para> HELM is distributed in the hope that it will be useful, but WITHOUT
+  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+  FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
+  more details.  </para>
 
+<para> You should have received a copy of the GNU General Public License
+  along with HELM; if not, write to the Free Software Foundation, Inc., 59
+  Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU
+  General Public License is available at <ulink type="help"
+    url="ghelp:gpl">this link</ulink>. </para>
index 1034d910b03c117a47271d16ab723b38afe5b837..97b58e572a63c7cf8db2e720b3599adb0ccdb7ac 100644 (file)
@@ -1,13 +1,17 @@
 <?xml version="1.0"?>
 <!DOCTYPE article PUBLIC "-//OASIS//DTD DocBook XML V4.1.2//EN"
     "http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [
-  <!ENTITY legal SYSTEM "legal.xml">
-  <!ENTITY appversion "0.0">
-  <!ENTITY manrevision "0.0">
+
+  <!ENTITY license SYSTEM "legal.xml">
+  <!ENTITY intro SYSTEM "intro.xml">
+  <!ENTITY terms SYSTEM "terms.xml">
+  <!ENTITY tactics SYSTEM "tactics.xml">
+
+  <!ENTITY manrevision "0">
   <!ENTITY date "February 2006">
   <!ENTITY app "<application>Matita</application>">
   <!ENTITY appname "Matita">
-  <!ENTITY version "0.0">
+  <!ENTITY appversion SYSTEM "../../dist/version.txt">
 ]>
 
 <!-- =============Document Header ============================= -->
@@ -15,7 +19,7 @@
 <!-- please do not change the id; for translations, change lang to -->
 <!-- appropriate code -->
 <articleinfo>
- <title>&app; Manual V&manrevision;</title>
+ <title>&app; V&appversion; Manual (rev. &manrevision;)</title>
 
  <copyright>
   <year>2006</year>
     </publisher> 
 -->
 
-   &legal;
-   <!-- This file  contains link to license for the documentation (GNU FDL), and 
-        other legal stuff such as "NO WARRANTY" statement. Please do not change 
-       any of this. -->
+    <legalnotice>
+      &license;
+    </legalnotice>
 
     <authorgroup> 
       <author> 
@@ -88,7 +91,7 @@
     
 <revhistory>
       <revision> 
-       <revnumber>&appname; Manual V&manrevision;</revnumber> 
+       <revnumber>&appname; V&appversion; Manual (rev. &manrevision;)</revnumber> 
        <date>&date;</date> 
        <revdescription> 
          <para role="author">The HELM team
     section altogether -->
     <legalnotice> 
       <title>Feedback</title> 
-      <para>To report a bug or make a suggestion regarding the &app; application or
-       this manual, follow the directions in the 
-       <ulink url="http://mowgli.cs.unibo.it/bugs"
-         type="help">HELM Bugzilla Page</ulink>. 
+      <para>To report a bug or make a suggestion regarding the &app;
+       application or this manual, follow the directions in the
+       <ulink url="http://bugs.mowgli.cs.unibo.it" type="help">HELM Bug
+         Tracking System Page</ulink>. 
       </para>
 <!-- Translators may also add here feedback address for translations -->
     </legalnotice>
   </indexterm>
 
 <!-- ============= Document Body ============================= -->
-<!-- ============= Introduction ============================== -->
-<sect1 id="intro">
- <title>Introduction</title>
- <sect2 id="what">
-  <title>What is Matita?</title>
-  
-  <para>
-  <application>Matita</application> is a proof assistant for ...
-  </para>
-
- </sect2>
-</sect1>
-
-<!-- =========== Terms, declarations and definitions ============ -->
-<sect1 id="terms_decl_def">
- <title>Terms, definitions, declarations and proofs</title>
- <sect2 id="terms">
- <title>Terms</title>
- </sect2>
- <sect2 id="definitions">
- <title>Definitions</title>
- </sect2>
- <sect2 id="declarations">
- <title>Declarations (of inductive types)</title>
- </sect2>
- <sect2 id="proofs">
- <title>Proofs</title>
- </sect2>
-</sect1>
-
-<!-- ============ Tactics ====================== -->
-<sect1 id="tactics">
- <title>Tactics</title>
-
-  <sect2 id="tac_absurd">
-    <title>absurd &lt;term&gt;</title>
-    <para>The tactic <command>absurd</command> </para>
-<para>
-<ulink url="#terms">ciao</ulink>
-</para>
-  </sect2>
-  <sect2 id="tac_apply">
-    <title>apply &lt;term&gt;</title>
-    <para>The tactic <command>apply</command> </para>
-  </sect2>
-  <sect2 id="tac_assumption">
-    <title>assumption</title>
-    <para>The tactic <command>assumption</command> </para>
-  </sect2>
-  <sect2 id="tac_auto">
-    <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
-    <para>The tactic <command>auto</command> </para>
-  </sect2>
-  <sect2 id="tac_clear">
-    <title>clear &lt;id&gt;</title>
-    <para>The tactic <command>clear</command> </para>
-  </sect2>
-  <sect2 id="tac_clearbody">
-    <title>clearbody &lt;id&gt;</title>
-    <para>The tactic <command>clearbody</command> </para>
-  </sect2>
-  <sect2 id="tac_change">
-    <title>change &lt;pattern&gt; with &lt;term&gt;</title>
-    <para>The tactic <command>change</command> </para>
-  </sect2>
-  <sect2 id="tac_compare">
-    <title>compare &lt;term&gt;</title>
-    <para>The tactic <command>compare</command> </para>
-  </sect2>
-  <sect2 id="tac_constructor">
-    <title>constructor &lt;int&gt;</title>
-    <para>The tactic <command>constructor</command> </para>
-  </sect2>
-  <sect2 id="tac_contradiction">
-    <title>contradiction</title>
-    <para>The tactic <command>contradiction</command> </para>
-  </sect2>
-  <sect2 id="tac_cut">
-    <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
-    <para>The tactic <command>cut</command> </para>
-  </sect2>
-  <sect2 id="tac_decide equality">
-    <title>decide</title>
-    <para>The tactic <command>decide equality</command> </para>
-  </sect2>
-  <sect2 id="tac_decompose">
-    <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
-    <para>The tactic <command>decompose</command> </para>
-  </sect2>
-  <sect2 id="tac_discriminate">
-    <title>discriminate &lt;term&gt;</title>
-    <para>The tactic <command>discriminate</command> </para>
-  </sect2>
-  <sect2 id="tac_elim">
-    <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
-    <para>The tactic <command>elim</command> </para>
-  </sect2>
-  <sect2 id="tac_elimType">
-    <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
-    <para>The tactic <command>elimType</command> </para>
-  </sect2>
-  <sect2 id="tac_exact">
-    <title>exact &lt;term&gt;</title>
-    <para>The tactic <command>exact</command> </para>
-  </sect2>
-  <sect2 id="tac_exists">
-    <title>exists</title>
-    <para>The tactic <command>exists</command> </para>
-  </sect2>
-  <sect2 id="tac_fail">
-    <title>fail</title>
-    <para>The tactic <command>fail</command> </para>
-  </sect2>
-  <sect2 id="tac_fold">
-    <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
-    <para>The tactic <command>fold</command> </para>
-  </sect2>
-  <sect2 id="tac_fourier">
-    <title>fourier</title>
-    <para>The tactic <command>fourier</command> </para>
-  </sect2>
-  <sect2 id="tac_fwd">
-    <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
-    <para>The tactic <command>fwd</command> </para>
-  </sect2>
-  <sect2 id="tac_generalize">
-    <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
-    <para>The tactic <command>generalize</command> </para>
-  </sect2>
-  <sect2 id="tac_id">
-    <title>id</title>
-    <para>The tactic <command>id</command> </para>
-  </sect2>
-  <sect2 id="tac_injection">
-    <title>injection &lt;term&gt;</title>
-    <para>The tactic <command>injection</command> </para>
-  </sect2>
-  <sect2 id="tac_intro">
-    <title>intro [&lt;ident&gt;]</title>
-    <para>The tactic <command>intro</command> </para>
-  </sect2>
-  <sect2 id="tac_intros">
-    <title>intros &lt;intros_spec&gt;</title>
-    <para>The tactic <command>intros</command> </para>
-  </sect2>
-  <sect2 id="tac_inversion">
-    <title>intros &lt;term&gt;</title>
-    <para>The tactic <command>intros</command> </para>
-  </sect2>
-  <sect2 id="tac_lapply">
-    <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
-    <para>The tactic <command>lapply</command> </para>
-  </sect2>
-  <sect2 id="tac_left">
-    <title>left</title>
-    <para>The tactic <command>left</command> </para>
-  </sect2>
-  <sect2 id="tac_letin">
-    <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
-    <para>The tactic <command>letin</command> </para>
-  </sect2>
-  <sect2 id="tac_normalize">
-    <title>normalize &lt;pattern&gt;</title>
-    <para>The tactic <command>normalize</command> </para>
-  </sect2>
-  <sect2 id="tac_paramodulation">
-    <title>paramodulation &lt;pattern&gt;</title>
-    <para>The tactic <command>paramodulation</command> </para>
-  </sect2>
-  <sect2 id="tac_reduce">
-    <title>reduce &lt;pattern&gt;</title>
-    <para>The tactic <command>reduce</command> </para>
-  </sect2>
-  <sect2 id="tac_reflexivity">
-    <title>reflexivity</title>
-    <para>The tactic <command>reflexivity</command> </para>
-  </sect2>
-  <sect2 id="tac_replace">
-    <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
-    <para>The tactic <command>replace</command> </para>
-  </sect2>
-  <sect2 id="tac_rewrite">
-    <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
-    <para>The tactic <command>rewrite</command> </para>
-  </sect2>
-  <sect2 id="tac_right">
-    <title>right</title>
-    <para>The tactic <command>right</command> </para>
-  </sect2>
-  <sect2 id="tac_ring">
-    <title>ring</title>
-    <para>The tactic <command>ring</command> </para>
-  </sect2>
-  <sect2 id="tac_simplify">
-    <title>simplify &lt;pattern&gt;</title>
-    <para>The tactic <command>simplify</command> </para>
-  </sect2>
-  <sect2 id="tac_split">
-    <title>split</title>
-    <para>The tactic <command>split</command> </para>
-  </sect2>
-  <sect2 id="tac_symmetry">
-    <title>symmetry</title>
-    <para>The tactic <command>symmetry</command> </para>
-  </sect2>
-  <sect2 id="tac_transitivity">
-    <title>transitivity &lt;term&gt;</title>
-    <para>The tactic <command>transitivity</command> </para>
-  </sect2>
-  <sect2 id="tac_unfold">
-    <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
-    <para>The tactic <command>unfold</command> </para>
-  </sect2>
-  <sect2 id="tac_whd">
-    <title>whd &lt;pattern&gt;</title>
-    <para>The tactic <command>whd</command> </para>
-  </sect2>
 
-</sect1>
+&intro;
+&terms;
+&tactics;
 
  <!-- ============= Application License ============================= -->
 
  <sect1 id="license">
   <title>License</title>
-  <para>
-   This program is free software; you can redistribute it and/or
-   modify it under the terms of the <citetitle>GNU General Public
-   License</citetitle> as published by the Free Software Foundation;
-   either version 2 of the License, or (at your option) any later
-   version.
-  </para>
-  <para>
-   This program is distributed in the hope that it will be useful, but
-   WITHOUT ANY WARRANTY; without even the implied warranty of
-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-   <citetitle>GNU General Public License</citetitle> for more details.
-  </para>
-  <para>
-   A copy of the <citetitle>GNU General Public License</citetitle> is
-   included as an appendix to the <citetitle>GNOME Users
-   Guide</citetitle>.  You may also obtain a copy of the
-   <citetitle>GNU General Public License</citetitle> from the Free
-   Software Foundation by visiting <ulink type="http"
-   url="http://www.fsf.org">their Web site</ulink> or by writing to
-   <address>
-    Free Software Foundation, Inc.
-    <street>59 Temple Place</street> - Suite 330
-    <city>Boston</city>, <state>MA</state> <postcode>02111-1307</postcode>
-    <country>USA</country>
-   </address>
-  </para>
+  &license;
  </sect1>
 </article>
 
diff --git a/helm/software/matita/help/C/tactics.xml b/helm/software/matita/help/C/tactics.xml
new file mode 100644 (file)
index 0000000..a423f37
--- /dev/null
@@ -0,0 +1,189 @@
+
+<!-- ============ Tactics ====================== -->
+<sect1 id="tactics">
+ <title>Tactics</title>
+
+  <sect2 id="tac_absurd">
+    <title>absurd &lt;term&gt;</title>
+    <para>The tactic <command>absurd</command> </para>
+<para>
+</para>
+  </sect2>
+  <sect2 id="tac_apply">
+    <title>apply &lt;term&gt;</title>
+    <para>The tactic <command>apply</command> </para>
+  </sect2>
+  <sect2 id="tac_assumption">
+    <title>assumption</title>
+    <para>The tactic <command>assumption</command> </para>
+  </sect2>
+  <sect2 id="tac_auto">
+    <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
+    <para>The tactic <command>auto</command> </para>
+  </sect2>
+  <sect2 id="tac_clear">
+    <title>clear &lt;id&gt;</title>
+    <para>The tactic <command>clear</command> </para>
+  </sect2>
+  <sect2 id="tac_clearbody">
+    <title>clearbody &lt;id&gt;</title>
+    <para>The tactic <command>clearbody</command> </para>
+  </sect2>
+  <sect2 id="tac_change">
+    <title>change &lt;pattern&gt; with &lt;term&gt;</title>
+    <para>The tactic <command>change</command> </para>
+  </sect2>
+  <sect2 id="tac_compare">
+    <title>compare &lt;term&gt;</title>
+    <para>The tactic <command>compare</command> </para>
+  </sect2>
+  <sect2 id="tac_constructor">
+    <title>constructor &lt;int&gt;</title>
+    <para>The tactic <command>constructor</command> </para>
+  </sect2>
+  <sect2 id="tac_contradiction">
+    <title>contradiction</title>
+    <para>The tactic <command>contradiction</command> </para>
+  </sect2>
+  <sect2 id="tac_cut">
+    <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
+    <para>The tactic <command>cut</command> </para>
+  </sect2>
+  <sect2 id="tac_decide_equality">
+    <title>decide</title>
+    <para>The tactic <command>decide equality</command> </para>
+  </sect2>
+  <sect2 id="tac_decompose">
+    <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
+    <para>The tactic <command>decompose</command> </para>
+  </sect2>
+  <sect2 id="tac_discriminate">
+    <title>discriminate &lt;term&gt;</title>
+    <para>The tactic <command>discriminate</command> </para>
+  </sect2>
+  <sect2 id="tac_elim">
+    <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
+    <para>The tactic <command>elim</command> </para>
+  </sect2>
+  <sect2 id="tac_elimType">
+    <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
+    <para>The tactic <command>elimType</command> </para>
+  </sect2>
+  <sect2 id="tac_exact">
+    <title>exact &lt;term&gt;</title>
+    <para>The tactic <command>exact</command> </para>
+  </sect2>
+  <sect2 id="tac_exists">
+    <title>exists</title>
+    <para>The tactic <command>exists</command> </para>
+  </sect2>
+  <sect2 id="tac_fail">
+    <title>fail</title>
+    <para>The tactic <command>fail</command> </para>
+  </sect2>
+  <sect2 id="tac_fold">
+    <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
+    <para>The tactic <command>fold</command> </para>
+  </sect2>
+  <sect2 id="tac_fourier">
+    <title>fourier</title>
+    <para>The tactic <command>fourier</command> </para>
+  </sect2>
+  <sect2 id="tac_fwd">
+    <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
+    <para>The tactic <command>fwd</command> </para>
+  </sect2>
+  <sect2 id="tac_generalize">
+    <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
+    <para>The tactic <command>generalize</command> </para>
+  </sect2>
+  <sect2 id="tac_id">
+    <title>id</title>
+    <para>The tactic <command>id</command> </para>
+  </sect2>
+  <sect2 id="tac_injection">
+    <title>injection &lt;term&gt;</title>
+    <para>The tactic <command>injection</command> </para>
+  </sect2>
+  <sect2 id="tac_intro">
+    <title>intro [&lt;ident&gt;]</title>
+    <para>The tactic <command>intro</command> </para>
+  </sect2>
+  <sect2 id="tac_intros">
+    <title>intros &lt;intros_spec&gt;</title>
+    <para>The tactic <command>intros</command> </para>
+  </sect2>
+  <sect2 id="tac_inversion">
+    <title>intros &lt;term&gt;</title>
+    <para>The tactic <command>intros</command> </para>
+  </sect2>
+  <sect2 id="tac_lapply">
+    <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
+    <para>The tactic <command>lapply</command> </para>
+  </sect2>
+  <sect2 id="tac_left">
+    <title>left</title>
+    <para>The tactic <command>left</command> </para>
+  </sect2>
+  <sect2 id="tac_letin">
+    <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
+    <para>The tactic <command>letin</command> </para>
+  </sect2>
+  <sect2 id="tac_normalize">
+    <title>normalize &lt;pattern&gt;</title>
+    <para>The tactic <command>normalize</command> </para>
+  </sect2>
+  <sect2 id="tac_paramodulation">
+    <title>paramodulation &lt;pattern&gt;</title>
+    <para>The tactic <command>paramodulation</command> </para>
+  </sect2>
+  <sect2 id="tac_reduce">
+    <title>reduce &lt;pattern&gt;</title>
+    <para>The tactic <command>reduce</command> </para>
+  </sect2>
+  <sect2 id="tac_reflexivity">
+    <title>reflexivity</title>
+    <para>The tactic <command>reflexivity</command> </para>
+  </sect2>
+  <sect2 id="tac_replace">
+    <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
+    <para>The tactic <command>replace</command> </para>
+  </sect2>
+  <sect2 id="tac_rewrite">
+    <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
+    <para>The tactic <command>rewrite</command> </para>
+  </sect2>
+  <sect2 id="tac_right">
+    <title>right</title>
+    <para>The tactic <command>right</command> </para>
+  </sect2>
+  <sect2 id="tac_ring">
+    <title>ring</title>
+    <para>The tactic <command>ring</command> </para>
+  </sect2>
+  <sect2 id="tac_simplify">
+    <title>simplify &lt;pattern&gt;</title>
+    <para>The tactic <command>simplify</command> </para>
+  </sect2>
+  <sect2 id="tac_split">
+    <title>split</title>
+    <para>The tactic <command>split</command> </para>
+  </sect2>
+  <sect2 id="tac_symmetry">
+    <title>symmetry</title>
+    <para>The tactic <command>symmetry</command> </para>
+  </sect2>
+  <sect2 id="tac_transitivity">
+    <title>transitivity &lt;term&gt;</title>
+    <para>The tactic <command>transitivity</command> </para>
+  </sect2>
+  <sect2 id="tac_unfold">
+    <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
+    <para>The tactic <command>unfold</command> </para>
+  </sect2>
+  <sect2 id="tac_whd">
+    <title>whd &lt;pattern&gt;</title>
+    <para>The tactic <command>whd</command> </para>
+  </sect2>
+
+</sect1>
diff --git a/helm/software/matita/help/C/terms.xml b/helm/software/matita/help/C/terms.xml
new file mode 100644 (file)
index 0000000..d92518d
--- /dev/null
@@ -0,0 +1,28 @@
+
+<!-- =========== Terms, declarations and definitions ============ -->
+
+<sect1 id="sec_terms">
+  <title>Terms, definitions, declarations and proofs</title>
+
+  <sect2 id="terms">
+    <title>Terms</title>
+    <para> TODO </para>
+  </sect2>
+
+  <sect2 id="definitions">
+    <title>Definitions</title>
+    <para> TODO </para>
+  </sect2>
+
+  <sect2 id="declarations">
+    <title>Declarations (of inductive types)</title>
+    <para> TODO </para>
+  </sect2>
+
+  <sect2 id="proofs">
+    <title>Proofs</title>
+    <para> TODO </para>
+  </sect2>
+
+</sect1>
+