X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_gettingstarted.xml;h=5f9dda35a829d1a6ba7fc86093841f1740de8fe6;hb=871ed1c297e8c929a8c4460162e8521c9656bbc0;hp=f7d435e70733439a4230046d57cee1ae42fe256f;hpb=c52baa34c7363fa58f81aea95bb0d72e10afdaf1;p=helm.git

diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml
index f7d435e70..5f9dda35a 100644
--- a/helm/software/matita/help/C/sec_gettingstarted.xml
+++ b/helm/software/matita/help/C/sec_gettingstarted.xml
@@ -11,23 +11,22 @@
 
   <sect1 id="unicode">
    <title>How to type Unicode symbols</title>
-   Unicode characters can be typed in several ways:
+   <para>Unicode characters can be typed in several ways:</para>
     <itemizedlist>
-     <listitem>Using the &quot;Shift+Ctrl+Unicode code&quot; standard
-      Gnome shortcut. E.g. Shift+Ctrl+3a9 generates &quot;Ω&quot;.
+      <listitem><para>Using the &quot;Shift+Ctrl+Unicode code&quot; standard Gnome shortcut. E.g. Shift+Ctrl+3a9 generates &quot;Ω&quot;.</para>
      </listitem>
-     <listitem>Typing the ligature &quot;\name&quot; where &quot;name&quot;
+     <listitem><para>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;.
+      &quot;Ω&quot;.</para>
      </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><para>Typing one of the following ligatures (and optionally
+         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;).</para>
      </listitem>
     </itemizedlist>
   </sect1>
@@ -67,29 +66,32 @@
      an action in the drop down menu right of it.</para>
     <sect3 id="locate">
      <title>Searching by name</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="hint">
      <title>List of lemmas that can be applied</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="match">
      <title>Searching by exact match</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="elim">
      <title>List of elimination principles for a given type</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
     <sect3 id="instance">
      <title>Searching by instantiation</title>
-     &TODO;
-    </sect3>
+     <para>     &TODO;</para>
+   </sect3>
    </sect2>
   </sect1>
   <sect1 id="authoring">
    <title>Authoring</title>
-   &TODO;
-  </sect1>
+   <sect2 id="developments">
+   <title>How to use developments</title>
+   <para>   &TODO;</para>
+ </sect2>
+ </sect1>
 </chapter>