--- /dev/null
+ <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>
+
--- /dev/null
+<?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 <term></title>
+ <para>The tactic <command>absurd</command> </para>
+<para>
+<ulink url="#terms">ciao</ulink>
+</para>
+ </sect2>
+ <sect2 id="apply">
+ <title>apply <term></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=<int>] [width=<int>] [paramodulation] [full]</title>
+ <para>The tactic <command>auto</command> </para>
+ </sect2>
+ <sect2 id="clear">
+ <title>clear <id></title>
+ <para>The tactic <command>clear</command> </para>
+ </sect2>
+ <sect2 id="clearbody">
+ <title>clearbody <id></title>
+ <para>The tactic <command>clearbody</command> </para>
+ </sect2>
+ <sect2 id="change">
+ <title>change <pattern> with <term></title>
+ <para>The tactic <command>change</command> </para>
+ </sect2>
+ <sect2 id="compare">
+ <title>compare <term></title>
+ <para>The tactic <command>compare</command> </para>
+ </sect2>
+ <sect2 id="constructor">
+ <title>constructor <int></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 <term> [as <id>]</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 [<ident list>] <ident> [<intros_spec>]</title>
+ <para>The tactic <command>decompose</command> </para>
+ </sect2>
+ <sect2 id="discriminate">
+ <title>discriminate <term></title>
+ <para>The tactic <command>discriminate</command> </para>
+ </sect2>
+ <sect2 id="elim">
+ <title>elim <term> [using <term>] [<intros_spec>]</title>
+ <para>The tactic <command>elim</command> </para>
+ </sect2>
+ <sect2 id="elimType">
+ <title>elimType <term> [using <term>]</title>
+ <para>The tactic <command>elimType</command> </para>
+ </sect2>
+ <sect2 id="exact">
+ <title>exact <term></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 <reduction_kind> <term> <pattern></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 <ident> [<ident list>]</title>
+ <para>The tactic <command>fwd</command> </para>
+ </sect2>
+ <sect2 id="generalize">
+ <title>generalize <pattern> [as <id>]</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 <term></title>
+ <para>The tactic <command>injection</command> </para>
+ </sect2>
+ <sect2 id="intro">
+ <title>intro [<ident>]</title>
+ <para>The tactic <command>intro</command> </para>
+ </sect2>
+ <sect2 id="intros">
+ <title>intros <intros_spec></title>
+ <para>The tactic <command>intros</command> </para>
+ </sect2>
+ <sect2 id="inversion">
+ <title>intros <term></title>
+ <para>The tactic <command>intros</command> </para>
+ </sect2>
+ <sect2 id="lapply">
+ <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</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 <ident> ≝ <term></title>
+ <para>The tactic <command>letin</command> </para>
+ </sect2>
+ <sect2 id="normalize">
+ <title>normalize <pattern></title>
+ <para>The tactic <command>normalize</command> </para>
+ </sect2>
+ <sect2 id="paramodulation">
+ <title>paramodulation <pattern></title>
+ <para>The tactic <command>paramodulation</command> </para>
+ </sect2>
+ <sect2 id="reduce">
+ <title>reduce <pattern></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 <pattern> with <term></title>
+ <para>The tactic <command>replace</command> </para>
+ </sect2>
+ <sect2 id="rewrite">
+ <title>rewrite {<|>} <term> <pattern></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 <pattern></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 <term></title>
+ <para>The tactic <command>transitivity</command> </para>
+ </sect2>
+ <sect2 id="unfold">
+ <title>unfold [<term>] <pattern></title>
+ <para>The tactic <command>unfold</command> </para>
+ </sect2>
+ <sect2 id="whd">
+ <title>whd <pattern></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>
+
+-->
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<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>
<keyword>injection</keyword>
<keyword>intro</keyword>
<keyword>intros</keyword>
+ <keyword>inversion</keyword>
<keyword>lapply</keyword>
<keyword>left</keyword>
<keyword>letin</keyword>
~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 () =
projects / helm.git / commitdiff