first sketch of the documentation (to be used by yelp)

diff --git a/helm/software/matita/help/C/legal.xml b/helm/software/matita/help/C/legal.xml
new file mode 100644 (file)
index 0000000..ac97e1d
--- /dev/null
+++ b/helm/software/matita/help/C/legal.xml
@@ -0,0 +1,76 @@
+  <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>
+         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>
+         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>
+

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
new file mode 100644 (file)
index 0000000..7f90e51
--- /dev/null
+++ b/helm/software/matita/help/C/matita.xml
@@ -0,0 +1,432 @@
+<?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 date "February 2006">
+  <!ENTITY app "<application>Matita</application>">
+  <!ENTITY appname "Matita">
+  <!ENTITY version "0.0">
+]>
+
+<!-- =============Document Header ============================= -->
+<article id="index" lang="en">
+<!-- please do not change the id; for translations, change lang to -->
+<!-- appropriate code -->
+<articleinfo>
+ <title>&app; Manual V&manrevision;</title>
+
+ <copyright>
+  <year>2006</year>
+  <holder>The HELM team.</holder>
+ </copyright>
+<!-- translators: uncomment this:
+
+  <copyright>
+   <year>2002</year>
+   <holder>ME-THE-TRANSLATOR (Latin translation)</holder>
+  </copyright>
+
+   -->
+<!-- An address can be added to the publisher information.  If a role is 
+     not specified, the publisher/author is the same for all versions of the 
+     document.  -->
+<!-- CSC:
+    <publisher> 
+      <publishername> GNOME Documentation Project </publishername> 
+    </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. -->
+
+    <authorgroup> 
+      <author> 
+       <firstname>Andrea</firstname> 
+       <surname>Asperti</surname> 
+       <affiliation> 
+         <address> <email>asperti@cs.unibo.it</email> </address> 
+       </affiliation> 
+      </author> 
+      <author> 
+       <firstname>Claudio</firstname> 
+       <surname>Sacerdoti Coen</surname> 
+       <affiliation> 
+         <address> <email>sacerdot@cs.unibo.it</email> </address> 
+       </affiliation> 
+      </author> 
+      <author> 
+       <firstname>Enrico</firstname> 
+       <surname>Tassi</surname> 
+       <affiliation> 
+         <address> <email>tassi@cs.unibo.it</email> </address> 
+       </affiliation> 
+      </author> 
+      <author> 
+       <firstname>Stefano</firstname> 
+       <surname>Zacchiroli</surname> 
+       <affiliation> 
+         <address> <email>zacchiro@cs.unibo.it</email> </address> 
+       </affiliation> 
+      </author> 
+<!-- This is appropriate place for other contributors: translators,
+      maintainers,  etc. Commented out by default.
+       <othercredit role="translator">
+       <firstname>Latin</firstname> 
+       <surname>Translator 1</surname> 
+       <affiliation> 
+         <orgname>Latin Translation Team</orgname> 
+         <address> <email>translator@gnome.org</email> </address> 
+       </affiliation>
+       <contrib>Latin translation</contrib>
+      </othercredit>
+-->
+    </authorgroup>
+    
+<revhistory>
+      <revision> 
+       <revnumber>&appname; Manual V&manrevision;</revnumber> 
+       <date>&date;</date> 
+       <revdescription> 
+         <para role="author">The HELM team
+<!--
+           <email>baudais@okstate.edu</email>
+-->
+         </para>
+<!--
+         <para role="publisher">GNOME Documentation Project</para>
+-->
+       </revdescription> 
+      </revision>
+  <revision>
+   <revnumber>0.0</revnumber>
+   <date>4 February 2006</date>
+   <authorinitials>HELM</authorinitials>
+   <revremark>
+   First draft completed.
+   </revremark>
+  </revision>
+
+ </revhistory>
+
+    <releaseinfo>This manual describes version &appversion; of &appname;.
+    </releaseinfo>
+    <!-- The following feedback information only applies to appliactions
+    listed in bugzilla.gnome.org and bugzilla.ximian.com. For other
+    applications, please provide your own feedback info or remove thsi
+    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>
+<!-- Translators may also add here feedback address for translations -->
+    </legalnotice>
+
+</articleinfo>
+
+  <indexterm zone="index"> 
+    <primary>Matita</primary> 
+  </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="absurd">
+    <title>absurd &lt;term&gt;</title>
+    <para>The tactic <command>absurd</command> </para>
+<para>
+<ulink url="#terms">ciao</ulink>
+</para>
+  </sect2>
+  <sect2 id="apply">
+    <title>apply &lt;term&gt;</title>
+    <para>The tactic <command>apply</command> </para>
+  </sect2>
+  <sect2 id="assumption">
+    <title>assumption</title>
+    <para>The tactic <command>assumption</command> </para>
+  </sect2>
+  <sect2 id="auto">
+    <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
+    <para>The tactic <command>auto</command> </para>
+  </sect2>
+  <sect2 id="clear">
+    <title>clear &lt;id&gt;</title>
+    <para>The tactic <command>clear</command> </para>
+  </sect2>
+  <sect2 id="clearbody">
+    <title>clearbody &lt;id&gt;</title>
+    <para>The tactic <command>clearbody</command> </para>
+  </sect2>
+  <sect2 id="change">
+    <title>change &lt;pattern&gt; with &lt;term&gt;</title>
+    <para>The tactic <command>change</command> </para>
+  </sect2>
+  <sect2 id="compare">
+    <title>compare &lt;term&gt;</title>
+    <para>The tactic <command>compare</command> </para>
+  </sect2>
+  <sect2 id="constructor">
+    <title>constructor &lt;int&gt;</title>
+    <para>The tactic <command>constructor</command> </para>
+  </sect2>
+  <sect2 id="contradiction">
+    <title>contradiction</title>
+    <para>The tactic <command>contradiction</command> </para>
+  </sect2>
+  <sect2 id="cut">
+    <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
+    <para>The tactic <command>cut</command> </para>
+  </sect2>
+  <sect2 id="decide equality">
+    <title>decide</title>
+    <para>The tactic <command>decide equality</command> </para>
+  </sect2>
+  <sect2 id="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="discriminate">
+    <title>discriminate &lt;term&gt;</title>
+    <para>The tactic <command>discriminate</command> </para>
+  </sect2>
+  <sect2 id="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="elimType">
+    <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
+    <para>The tactic <command>elimType</command> </para>
+  </sect2>
+  <sect2 id="exact">
+    <title>exact &lt;term&gt;</title>
+    <para>The tactic <command>exact</command> </para>
+  </sect2>
+  <sect2 id="exists">
+    <title>exists</title>
+    <para>The tactic <command>exists</command> </para>
+  </sect2>
+  <sect2 id="fail">
+    <title>fail</title>
+    <para>The tactic <command>fail</command> </para>
+  </sect2>
+  <sect2 id="fold">
+    <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
+    <para>The tactic <command>fold</command> </para>
+  </sect2>
+  <sect2 id="fourier">
+    <title>fourier</title>
+    <para>The tactic <command>fourier</command> </para>
+  </sect2>
+  <sect2 id="fwd">
+    <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
+    <para>The tactic <command>fwd</command> </para>
+  </sect2>
+  <sect2 id="generalize">
+    <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
+    <para>The tactic <command>generalize</command> </para>
+  </sect2>
+  <sect2 id="id">
+    <title>id</title>
+    <para>The tactic <command>id</command> </para>
+  </sect2>
+  <sect2 id="injection">
+    <title>injection &lt;term&gt;</title>
+    <para>The tactic <command>injection</command> </para>
+  </sect2>
+  <sect2 id="intro">
+    <title>intro [&lt;ident&gt;]</title>
+    <para>The tactic <command>intro</command> </para>
+  </sect2>
+  <sect2 id="intros">
+    <title>intros &lt;intros_spec&gt;</title>
+    <para>The tactic <command>intros</command> </para>
+  </sect2>
+  <sect2 id="inversion">
+    <title>intros &lt;term&gt;</title>
+    <para>The tactic <command>intros</command> </para>
+  </sect2>
+  <sect2 id="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="left">
+    <title>left</title>
+    <para>The tactic <command>left</command> </para>
+  </sect2>
+  <sect2 id="letin">
+    <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
+    <para>The tactic <command>letin</command> </para>
+  </sect2>
+  <sect2 id="normalize">
+    <title>normalize &lt;pattern&gt;</title>
+    <para>The tactic <command>normalize</command> </para>
+  </sect2>
+  <sect2 id="paramodulation">
+    <title>paramodulation &lt;pattern&gt;</title>
+    <para>The tactic <command>paramodulation</command> </para>
+  </sect2>
+  <sect2 id="reduce">
+    <title>reduce &lt;pattern&gt;</title>
+    <para>The tactic <command>reduce</command> </para>
+  </sect2>
+  <sect2 id="reflexivity">
+    <title>reflexivity</title>
+    <para>The tactic <command>reflexivity</command> </para>
+  </sect2>
+  <sect2 id="replace">
+    <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
+    <para>The tactic <command>replace</command> </para>
+  </sect2>
+  <sect2 id="rewrite">
+    <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
+    <para>The tactic <command>rewrite</command> </para>
+  </sect2>
+  <sect2 id="right">
+    <title>right</title>
+    <para>The tactic <command>right</command> </para>
+  </sect2>
+  <sect2 id="ring">
+    <title>ring</title>
+    <para>The tactic <command>ring</command> </para>
+  </sect2>
+  <sect2 id="simplify">
+    <title>simplify &lt;pattern&gt;</title>
+    <para>The tactic <command>simplify</command> </para>
+  </sect2>
+  <sect2 id="split">
+    <title>split</title>
+    <para>The tactic <command>split</command> </para>
+  </sect2>
+  <sect2 id="symmetry">
+    <title>symmetry</title>
+    <para>The tactic <command>symmetry</command> </para>
+  </sect2>
+  <sect2 id="transitivity">
+    <title>transitivity &lt;term&gt;</title>
+    <para>The tactic <command>transitivity</command> </para>
+  </sect2>
+  <sect2 id="unfold">
+    <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
+    <para>The tactic <command>unfold</command> </para>
+  </sect2>
+  <sect2 id="whd">
+    <title>whd &lt;pattern&gt;</title>
+    <para>The tactic <command>whd</command> </para>
+  </sect2>
+
+</sect1>
+
+ <!-- ============= 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>
+ </sect1>
+</article>
+
+<!-- CSC: valid element tags
+<sect1 id="intro"> <title>Introduction</title> ...
+<sect2 id="what"> <title>What is Matita?</title>
+<para>
+<note> <title>Note:</title> <para> ...
+<footnote> <para> ...
+<itemizedlist mark="opencircle">
+    <listitem>
+     <para>
+       The computer player for Iagno is easy to beat.
+     </para>
+    </listitem>
+ </itemizedlist>
+
+<ulink type="http" url="http://www.gnome.org/gdp">
+<email>itp@gnu.org</email>
+<application>Matita</application>
+<command>iagno</command> on the command line
+<citetitle>Othello</citetitle>
+
+<guimenuitem>Iagno</guimenuitem>
+<guisubmenu>Games</guisubmenu>
+<guibutton>none</guibutton>
+<menuchoice> <guimenu>Settings</guimenu> <guisubmenu>Preferences </guisubmenu> </menuchoice>
+
+<xref linkend="start-shot"/>. 
+<figure id="start-shot">
+ <title>Starting Position</title>
+ <screenshot>
+   <mediaobject> 
+   <imageobject>
+ <imagedata fileref="figures/START.png" format="PNG" srccredit="Eric Baudais"/>
+  </imageobject>
+   <textobject> 
+     <phrase>Screenshot of the starting position.</phrase> 
+   </textobject> 
+ </mediaobject>
+ </screenshot>
+</figure>
+
+-->

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 436dd7b268b664c5cea6a27ebcc6f83b5eb44fb1..71506d55ac3b0f0784755299fd7ba00f36b63135 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -877,7 +877,7 @@
                              <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image856">
+                               <widget class="GtkImage" id="image889">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-new</property>
                                  <property name="icon_size">1</property>
@@ -898,7 +898,7 @@
                              <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image857">
+                               <widget class="GtkImage" id="image890">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-open</property>
                                  <property name="icon_size">1</property>
@@ -919,7 +919,7 @@
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image858">
+                               <widget class="GtkImage" id="image891">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save</property>
                                  <property name="icon_size">1</property>
@@ -940,7 +940,7 @@
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image859">
+                               <widget class="GtkImage" id="image892">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save-as</property>
                                  <property name="icon_size">1</property>
@@ -961,7 +961,7 @@
                              <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image860">
+                               <widget class="GtkImage" id="image893">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-execute</property>
                                  <property name="icon_size">1</property>
@@ -988,7 +988,7 @@
                              <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image861">
+                               <widget class="GtkImage" id="image894">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-quit</property>
                                  <property name="icon_size">1</property>
@@ -1023,7 +1023,7 @@
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image862">
+                               <widget class="GtkImage" id="image895">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-undo</property>
                                  <property name="icon_size">1</property>
@@ -1045,7 +1045,7 @@
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image863">
+                               <widget class="GtkImage" id="image896">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-redo</property>
                                  <property name="icon_size">1</property>
@@ -1072,7 +1072,7 @@
                              <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image864">
+                               <widget class="GtkImage" id="image897">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-cut</property>
                                  <property name="icon_size">1</property>
@@ -1093,7 +1093,7 @@
                              <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image865">
+                               <widget class="GtkImage" id="image898">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-copy</property>
                                  <property name="icon_size">1</property>
@@ -1114,7 +1114,7 @@
                              <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image866">
+                               <widget class="GtkImage" id="image899">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-paste</property>
                                  <property name="icon_size">1</property>
@@ -1142,7 +1142,7 @@
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image867">
+                               <widget class="GtkImage" id="image900">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-delete</property>
                                  <property name="icon_size">1</property>
@@ -1183,7 +1183,7 @@
                              <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image868">
+                               <widget class="GtkImage" id="image901">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-find-and-replace</property>
                                  <property name="icon_size">1</property>
@@ -1352,7 +1352,7 @@
                              <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image869">
+                               <widget class="GtkImage" id="image902">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-in</property>
                                  <property name="icon_size">1</property>
@@ -1374,7 +1374,7 @@
                              <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image870">
+                               <widget class="GtkImage" id="image903">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-out</property>
                                  <property name="icon_size">1</property>
@@ -1395,7 +1395,7 @@
                              <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image871">
+                               <widget class="GtkImage" id="image904">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-100</property>
                                  <property name="icon_size">1</property>
@@ -1440,6 +1440,27 @@
                      <child>
                        <widget class="GtkMenu" id="helpMenu_menu">
 
+                         <child>
+                           <widget class="GtkImageMenuItem" id="contentsMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">_Contents</property>
+                             <property name="use_underline">True</property>
+                             <accelerator key="F1" modifiers="0" signal="activate"/>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image905">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-help</property>
+                                 <property name="icon_size">1</property>
+                                 <property name="xalign">0.5</property>
+                                 <property name="yalign">0.5</property>
+                                 <property name="xpad">0</property>
+                                 <property name="ypad">0</property>
+                               </widget>
+                             </child>
+                           </widget>
+                         </child>
+
                          <child>
                            <widget class="GtkImageMenuItem" id="aboutMenuItem">
                              <property name="visible">True</property>
@@ -1447,7 +1468,7 @@
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image872">
+                               <widget class="GtkImage" id="image906">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-about</property>
                                  <property name="icon_size">1</property>

diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index 0c181ee4480269bf55ec473df745108fc03e825e..d0223158856eeee49980978b26deaa3eee60357d 100644 (file)
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -108,6 +108,7 @@
     <keyword>injection</keyword>
     <keyword>intro</keyword>
     <keyword>intros</keyword>
+    <keyword>inversion</keyword>
     <keyword>lapply</keyword>
     <keyword>left</keyword>
     <keyword>letin</keyword>

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 34406a3cd147908ef96d76a9804ecafc3064815f..9cde82b7535501fb100d9a3a121621fff0d1b301 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -206,6 +206,8 @@ class gui () =
         ~website:"http://helm.cs.unibo.it"
         ()
       in
+      connect_menu_item main#contentsMenuItem
+       (fun () -> ignore (Sys.command "gnome-help ghelp:///home/claudio/miohelm/matita/help/C/matita.xml &"));
       connect_menu_item main#aboutMenuItem about_dialog#present;
         (* findRepl win *)
       let show_find_Repl () =