]> matita.cs.unibo.it Git - helm.git/blob - matita/help/C/matita.xml
first sketch of the documentation (to be used by yelp)
[helm.git] / matita / help / C / matita.xml
1 <?xml version="1.0"?>
2 <!DOCTYPE article PUBLIC "-//OASIS//DTD DocBook XML V4.1.2//EN"
3     "http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [
4   <!ENTITY legal SYSTEM "legal.xml">
5   <!ENTITY appversion "0.0">
6   <!ENTITY manrevision "0.0">
7   <!ENTITY date "February 2006">
8   <!ENTITY app "<application>Matita</application>">
9   <!ENTITY appname "Matita">
10   <!ENTITY version "0.0">
11 ]>
12
13 <!-- =============Document Header ============================= -->
14 <article id="index" lang="en">
15 <!-- please do not change the id; for translations, change lang to -->
16 <!-- appropriate code -->
17 <articleinfo>
18  <title>&app; Manual V&manrevision;</title>
19
20  <copyright>
21   <year>2006</year>
22   <holder>The HELM team.</holder>
23  </copyright>
24 <!-- translators: uncomment this:
25
26   <copyright>
27    <year>2002</year>
28    <holder>ME-THE-TRANSLATOR (Latin translation)</holder>
29   </copyright>
30
31    -->
32 <!-- An address can be added to the publisher information.  If a role is 
33      not specified, the publisher/author is the same for all versions of the 
34      document.  -->
35 <!-- CSC:
36     <publisher> 
37       <publishername> GNOME Documentation Project </publishername> 
38     </publisher> 
39 -->
40
41    &legal;
42    <!-- This file  contains link to license for the documentation (GNU FDL), and 
43         other legal stuff such as "NO WARRANTY" statement. Please do not change 
44         any of this. -->
45
46     <authorgroup> 
47       <author> 
48         <firstname>Andrea</firstname> 
49         <surname>Asperti</surname> 
50         <affiliation> 
51           <address> <email>asperti@cs.unibo.it</email> </address> 
52         </affiliation> 
53       </author> 
54       <author> 
55         <firstname>Claudio</firstname> 
56         <surname>Sacerdoti Coen</surname> 
57         <affiliation> 
58           <address> <email>sacerdot@cs.unibo.it</email> </address> 
59         </affiliation> 
60       </author> 
61       <author> 
62         <firstname>Enrico</firstname> 
63         <surname>Tassi</surname> 
64         <affiliation> 
65           <address> <email>tassi@cs.unibo.it</email> </address> 
66         </affiliation> 
67       </author> 
68       <author> 
69         <firstname>Stefano</firstname> 
70         <surname>Zacchiroli</surname> 
71         <affiliation> 
72           <address> <email>zacchiro@cs.unibo.it</email> </address> 
73         </affiliation> 
74       </author> 
75 <!-- This is appropriate place for other contributors: translators,
76       maintainers,  etc. Commented out by default.
77        <othercredit role="translator">
78         <firstname>Latin</firstname> 
79         <surname>Translator 1</surname> 
80         <affiliation> 
81           <orgname>Latin Translation Team</orgname> 
82           <address> <email>translator@gnome.org</email> </address> 
83         </affiliation>
84         <contrib>Latin translation</contrib>
85       </othercredit>
86 -->
87     </authorgroup>
88     
89 <revhistory>
90       <revision> 
91         <revnumber>&appname; Manual V&manrevision;</revnumber> 
92         <date>&date;</date> 
93         <revdescription> 
94           <para role="author">The HELM team
95 <!--
96             <email>baudais@okstate.edu</email>
97 -->
98           </para>
99 <!--
100           <para role="publisher">GNOME Documentation Project</para>
101 -->
102         </revdescription> 
103       </revision>
104   <revision>
105    <revnumber>0.0</revnumber>
106    <date>4 February 2006</date>
107    <authorinitials>HELM</authorinitials>
108    <revremark>
109    First draft completed.
110    </revremark>
111   </revision>
112
113  </revhistory>
114
115     <releaseinfo>This manual describes version &appversion; of &appname;.
116     </releaseinfo>
117     <!-- The following feedback information only applies to appliactions
118     listed in bugzilla.gnome.org and bugzilla.ximian.com. For other
119     applications, please provide your own feedback info or remove thsi
120     section altogether -->
121     <legalnotice> 
122       <title>Feedback</title> 
123       <para>To report a bug or make a suggestion regarding the &app; application or
124         this manual, follow the directions in the 
125         <ulink url="http://mowgli.cs.unibo.it/bugs"
126           type="help">HELM Bugzilla Page</ulink>. 
127       </para>
128 <!-- Translators may also add here feedback address for translations -->
129     </legalnotice>
130
131 </articleinfo>
132
133   <indexterm zone="index"> 
134     <primary>Matita</primary> 
135   </indexterm>
136
137 <!-- ============= Document Body ============================= -->
138 <!-- ============= Introduction ============================== -->
139 <sect1 id="intro">
140  <title>Introduction</title>
141  <sect2 id="what">
142   <title>What is Matita?</title>
143   
144   <para>
145   <application>Matita</application> is a proof assistant for ...
146   </para>
147
148  </sect2>
149 </sect1>
150
151 <!-- =========== Terms, declarations and definitions ============ -->
152 <sect1 id="terms_decl_def">
153  <title>Terms, definitions, declarations and proofs</title>
154  <sect2 id="terms">
155  <title>Terms</title>
156  </sect2>
157  <sect2 id="definitions">
158  <title>Definitions</title>
159  </sect2>
160  <sect2 id="declarations">
161  <title>Declarations (of inductive types)</title>
162  </sect2>
163  <sect2 id="proofs">
164  <title>Proofs</title>
165  </sect2>
166 </sect1>
167
168 <!-- ============ Tactics ====================== -->
169 <sect1 id="tactics">
170  <title>Tactics</title>
171
172   <sect2 id="absurd">
173     <title>absurd &lt;term&gt;</title>
174     <para>The tactic <command>absurd</command> </para>
175 <para>
176 <ulink url="#terms">ciao</ulink>
177 </para>
178   </sect2>
179   <sect2 id="apply">
180     <title>apply &lt;term&gt;</title>
181     <para>The tactic <command>apply</command> </para>
182   </sect2>
183   <sect2 id="assumption">
184     <title>assumption</title>
185     <para>The tactic <command>assumption</command> </para>
186   </sect2>
187   <sect2 id="auto">
188     <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
189     <para>The tactic <command>auto</command> </para>
190   </sect2>
191   <sect2 id="clear">
192     <title>clear &lt;id&gt;</title>
193     <para>The tactic <command>clear</command> </para>
194   </sect2>
195   <sect2 id="clearbody">
196     <title>clearbody &lt;id&gt;</title>
197     <para>The tactic <command>clearbody</command> </para>
198   </sect2>
199   <sect2 id="change">
200     <title>change &lt;pattern&gt; with &lt;term&gt;</title>
201     <para>The tactic <command>change</command> </para>
202   </sect2>
203   <sect2 id="compare">
204     <title>compare &lt;term&gt;</title>
205     <para>The tactic <command>compare</command> </para>
206   </sect2>
207   <sect2 id="constructor">
208     <title>constructor &lt;int&gt;</title>
209     <para>The tactic <command>constructor</command> </para>
210   </sect2>
211   <sect2 id="contradiction">
212     <title>contradiction</title>
213     <para>The tactic <command>contradiction</command> </para>
214   </sect2>
215   <sect2 id="cut">
216     <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
217     <para>The tactic <command>cut</command> </para>
218   </sect2>
219   <sect2 id="decide equality">
220     <title>decide</title>
221     <para>The tactic <command>decide equality</command> </para>
222   </sect2>
223   <sect2 id="decompose">
224     <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
225     <para>The tactic <command>decompose</command> </para>
226   </sect2>
227   <sect2 id="discriminate">
228     <title>discriminate &lt;term&gt;</title>
229     <para>The tactic <command>discriminate</command> </para>
230   </sect2>
231   <sect2 id="elim">
232     <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
233     <para>The tactic <command>elim</command> </para>
234   </sect2>
235   <sect2 id="elimType">
236     <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
237     <para>The tactic <command>elimType</command> </para>
238   </sect2>
239   <sect2 id="exact">
240     <title>exact &lt;term&gt;</title>
241     <para>The tactic <command>exact</command> </para>
242   </sect2>
243   <sect2 id="exists">
244     <title>exists</title>
245     <para>The tactic <command>exists</command> </para>
246   </sect2>
247   <sect2 id="fail">
248     <title>fail</title>
249     <para>The tactic <command>fail</command> </para>
250   </sect2>
251   <sect2 id="fold">
252     <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
253     <para>The tactic <command>fold</command> </para>
254   </sect2>
255   <sect2 id="fourier">
256     <title>fourier</title>
257     <para>The tactic <command>fourier</command> </para>
258   </sect2>
259   <sect2 id="fwd">
260     <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
261     <para>The tactic <command>fwd</command> </para>
262   </sect2>
263   <sect2 id="generalize">
264     <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
265     <para>The tactic <command>generalize</command> </para>
266   </sect2>
267   <sect2 id="id">
268     <title>id</title>
269     <para>The tactic <command>id</command> </para>
270   </sect2>
271   <sect2 id="injection">
272     <title>injection &lt;term&gt;</title>
273     <para>The tactic <command>injection</command> </para>
274   </sect2>
275   <sect2 id="intro">
276     <title>intro [&lt;ident&gt;]</title>
277     <para>The tactic <command>intro</command> </para>
278   </sect2>
279   <sect2 id="intros">
280     <title>intros &lt;intros_spec&gt;</title>
281     <para>The tactic <command>intros</command> </para>
282   </sect2>
283   <sect2 id="inversion">
284     <title>intros &lt;term&gt;</title>
285     <para>The tactic <command>intros</command> </para>
286   </sect2>
287   <sect2 id="lapply">
288     <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
289     <para>The tactic <command>lapply</command> </para>
290   </sect2>
291   <sect2 id="left">
292     <title>left</title>
293     <para>The tactic <command>left</command> </para>
294   </sect2>
295   <sect2 id="letin">
296     <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
297     <para>The tactic <command>letin</command> </para>
298   </sect2>
299   <sect2 id="normalize">
300     <title>normalize &lt;pattern&gt;</title>
301     <para>The tactic <command>normalize</command> </para>
302   </sect2>
303   <sect2 id="paramodulation">
304     <title>paramodulation &lt;pattern&gt;</title>
305     <para>The tactic <command>paramodulation</command> </para>
306   </sect2>
307   <sect2 id="reduce">
308     <title>reduce &lt;pattern&gt;</title>
309     <para>The tactic <command>reduce</command> </para>
310   </sect2>
311   <sect2 id="reflexivity">
312     <title>reflexivity</title>
313     <para>The tactic <command>reflexivity</command> </para>
314   </sect2>
315   <sect2 id="replace">
316     <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
317     <para>The tactic <command>replace</command> </para>
318   </sect2>
319   <sect2 id="rewrite">
320     <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
321     <para>The tactic <command>rewrite</command> </para>
322   </sect2>
323   <sect2 id="right">
324     <title>right</title>
325     <para>The tactic <command>right</command> </para>
326   </sect2>
327   <sect2 id="ring">
328     <title>ring</title>
329     <para>The tactic <command>ring</command> </para>
330   </sect2>
331   <sect2 id="simplify">
332     <title>simplify &lt;pattern&gt;</title>
333     <para>The tactic <command>simplify</command> </para>
334   </sect2>
335   <sect2 id="split">
336     <title>split</title>
337     <para>The tactic <command>split</command> </para>
338   </sect2>
339   <sect2 id="symmetry">
340     <title>symmetry</title>
341     <para>The tactic <command>symmetry</command> </para>
342   </sect2>
343   <sect2 id="transitivity">
344     <title>transitivity &lt;term&gt;</title>
345     <para>The tactic <command>transitivity</command> </para>
346   </sect2>
347   <sect2 id="unfold">
348     <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
349     <para>The tactic <command>unfold</command> </para>
350   </sect2>
351   <sect2 id="whd">
352     <title>whd &lt;pattern&gt;</title>
353     <para>The tactic <command>whd</command> </para>
354   </sect2>
355
356 </sect1>
357
358  <!-- ============= Application License ============================= -->
359
360  <sect1 id="license">
361   <title>License</title>
362   <para>
363    This program is free software; you can redistribute it and/or
364    modify it under the terms of the <citetitle>GNU General Public
365    License</citetitle> as published by the Free Software Foundation;
366    either version 2 of the License, or (at your option) any later
367    version.
368   </para>
369   <para>
370    This program is distributed in the hope that it will be useful, but
371    WITHOUT ANY WARRANTY; without even the implied warranty of
372    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
373    <citetitle>GNU General Public License</citetitle> for more details.
374   </para>
375   <para>
376    A copy of the <citetitle>GNU General Public License</citetitle> is
377    included as an appendix to the <citetitle>GNOME Users
378    Guide</citetitle>.  You may also obtain a copy of the
379    <citetitle>GNU General Public License</citetitle> from the Free
380    Software Foundation by visiting <ulink type="http"
381    url="http://www.fsf.org">their Web site</ulink> or by writing to
382    <address>
383     Free Software Foundation, Inc.
384     <street>59 Temple Place</street> - Suite 330
385     <city>Boston</city>, <state>MA</state> <postcode>02111-1307</postcode>
386     <country>USA</country>
387    </address>
388   </para>
389  </sect1>
390 </article>
391
392 <!-- CSC: valid element tags
393 <sect1 id="intro"> <title>Introduction</title> ...
394 <sect2 id="what"> <title>What is Matita?</title>
395 <para>
396 <note> <title>Note:</title> <para> ...
397 <footnote> <para> ...
398 <itemizedlist mark="opencircle">
399     <listitem>
400      <para>
401         The computer player for Iagno is easy to beat.
402      </para>
403     </listitem>
404  </itemizedlist>
405
406 <ulink type="http" url="http://www.gnome.org/gdp">
407 <email>itp@gnu.org</email>
408 <application>Matita</application>
409 <command>iagno</command> on the command line
410 <citetitle>Othello</citetitle>
411
412 <guimenuitem>Iagno</guimenuitem>
413 <guisubmenu>Games</guisubmenu>
414 <guibutton>none</guibutton>
415 <menuchoice> <guimenu>Settings</guimenu> <guisubmenu>Preferences </guisubmenu> </menuchoice>
416
417 <xref linkend="start-shot"/>. 
418 <figure id="start-shot">
419  <title>Starting Position</title>
420  <screenshot>
421    <mediaobject> 
422    <imageobject>
423  <imagedata fileref="figures/START.png" format="PNG" srccredit="Eric Baudais"/>
424   </imageobject>
425    <textobject> 
426      <phrase>Screenshot of the starting position.</phrase> 
427    </textobject> 
428  </mediaobject>
429  </screenshot>
430 </figure>
431
432 -->