New documentation.

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 1120cb4ec64d26095ca3a58d75a28f8b89f2c1f4..41d763c9354658ca5fdb3b8fc699ae4eb69722db 100644 (file)
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -8,6 +8,9 @@
   <!ENTITY intro SYSTEM "sec_intro.xml">
   <!ENTITY terms SYSTEM "sec_terms.xml">
   <!ENTITY tactics SYSTEM "sec_tactics.xml">
+  <!ENTITY tacticals SYSTEM "sec_tacticals.xml">
+  <!ENTITY othercommands SYSTEM "sec_commands.xml">
+  <!ENTITY usernotation SYSTEM "sec_usernotation.xml">
 
   <!ENTITY manrevision "0">
   <!ENTITY date "February 2006">
@@ -156,7 +159,10 @@
 &install;
 &gettingstarted;
 &terms;
+&usernotation;
 &tactics;
+&tacticals;
+&othercommands;
 
  <!-- ============= Application License ============================= -->
 

diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
new file mode 100644 (file)
index 0000000..b1bada0
--- /dev/null
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -0,0 +1,7 @@
+
+<!-- ============ Commands ====================== -->
+<chapter id="sec_commands">
+ <title>Other commands</title>
+ &TODO;
+</chapter>
+

diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml
index b7b006590a39498117d0a7d267aaf6f293a66514..f7d435e70733439a4230046d57cee1ae42fe256f 100644 (file)
--- a/helm/software/matita/help/C/sec_gettingstarted.xml
+++ b/helm/software/matita/help/C/sec_gettingstarted.xml
@@ -3,10 +3,93 @@
 
 <chapter id="sec_gettingstarted">
   <title>Getting started</title>
+  <para> If you are already familiar with the Calculus of (co)Inductive
+  Constructions (CIC) and with interactive theorem provers with procedural
+  proof languages (expecially Coq), getting started with Matita is relatively
+  easy. You just need to learn how to type Unicode symbols, how to browse
+  and search the library and how to author a proof script.</para>
+
   <sect1 id="unicode">
    <title>How to type Unicode symbols</title>
+   Unicode characters can be typed in several ways:
+    <itemizedlist>
+     <listitem>Using the &quot;Shift+Ctrl+Unicode code&quot; standard
+      Gnome shortcut. E.g. Shift+Ctrl+3a9 generates &quot;Ω&quot;.
+     </listitem>
+     <listitem>Typing the ligature &quot;\name&quot; where &quot;name&quot;
+      is a standard Unicode or LaTeX name for the character. Pressing
+      &quot;Alt+L&quot; just after the last character of the name converts
+      the ligature to the Unicode symbol. This operation is
+      not required since Matita understands also the &quot;\name&quot;
+      sequences. E.g. &quot;\Omega&quot; followed by Alt+L generates
+      &quot;Ω&quot;.
+     </listitem>
+     <listitem>Typing one of the following ligatures (and opzionally converting
+      the ligature to the Unicode character has described before):
+      &quot;:=&quot; (which stands for ≝); &quot;->&quot; (which stands for &quot;→&quot;);
+      &quot;->&quot; (which stands for &quot;⇒&quot;).
+     </listitem>
+    </itemizedlist>
+  </sect1>
+  <sect1 id="cicbrowser">
+   <title>Browsing and searching</title>
+   <para>The CIC browser is used to browse and search the library.
+    You can open a new CIC browser selecting &quot;New Cic Browser&quot;
+    from the &quot;View&quot; menu of Matita, or by pressing &quot;F3&quot;.
+    The CIC browser is similar to a traditional Web browser.</para>
+   <sect2 id="browsinglib">
+    <title>Browsing the library</title>
+    <para>To browse the library, type in the location bar the absolute URI of
+    the theorem, definition or library fragment you are interested in.
+    &quot;cic:/&quot; is the root of the library. Contributions developed
+    in Matita are under &quot;cic:/matita&quot;; all the others are
+    part of the library of Coq.</para>
+    <para>Following the hyperlinks it is possible to navigate in the Web
+    of mathematical notions. Proof are rendered in pseudo-natural language
+    and mathematical notation is used for formulae. For now, mathematical
+    notation must be included in the current script to be activated, but we
+    plan to remove this limitation.</para>
+   </sect2>
+   <sect2 id="aboutproof">
+    <title>Looking at a proof under development</title>
+    <para>A proof under development is not yet part of the library.
+     The special URI &quot;about:proof&quot; can be used to browse the
+     proof currently under development, if there is one.
+     The &quot;home&quot; button of the CIC browser sets the location bar to
+     &quot;about:proof&quot;.
+    </para>
+   </sect2>
+   <sect2 id="whelp">
+    <title>Searching the library</title>
+    <para>The query bar of the CIC browser can be used to search the library
+     of Matita for theorems or definitions that match certain criteria.
+     The criteria is given by typing a term in the query bar and selecting
+     an action in the drop down menu right of it.</para>
+    <sect3 id="locate">
+     <title>Searching by name</title>
+     &TODO;
+    </sect3>
+    <sect3 id="hint">
+     <title>List of lemmas that can be applied</title>
+     &TODO;
+    </sect3>
+    <sect3 id="match">
+     <title>Searching by exact match</title>
+     &TODO;
+    </sect3>
+    <sect3 id="elim">
+     <title>List of elimination principles for a given type</title>
+     &TODO;
+    </sect3>
+    <sect3 id="instance">
+     <title>Searching by instantiation</title>
+     &TODO;
+    </sect3>
+   </sect2>
+  </sect1>
+  <sect1 id="authoring">
+   <title>Authoring</title>
    &TODO;
   </sect1>
-  &TODO;
 </chapter>
 

diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml
index 1695170887770b57480de9c1750227c89e49c738..a29b4960d1dede420648f00e6eb14720865b2ff5 100644 (file)
--- a/helm/software/matita/help/C/sec_intro.xml
+++ b/helm/software/matita/help/C/sec_intro.xml
@@ -56,7 +56,12 @@
      <listitem>an extensible language of tactics;</listitem>
      <listitem>automatic implicit arguments;</listitem>
      <listitem>several ad-hoc decision procedures;</listitem>
-     <listitem>several rarely used variants for most of the tactics.</listitem>
+     <listitem>several rarely used variants for most of the tactics;</listitem>
+     <listitem>sections and local variables. To maintain compatibility
+      with the library of Coq, theorems defined inside sections are abstracted
+      by name over the section variables; their instances are explicitly
+      applied to actual arguments by means of explicit named
+      substitutions.</listitem>
     </itemizedlist>
 
     <para>

diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
new file mode 100644 (file)
index 0000000..92698f8
--- /dev/null
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -0,0 +1,7 @@
+
+<!-- ============ User Notation ====================== -->
+<chapter id="sec_usernotation">
+ <title>Extending the syntax</title>
+ &TODO;
+</chapter>
+