]> matita.cs.unibo.it Git - helm.git/commitdiff
Attempt to make our markup respect the docbook specification(!), major changes
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 7 Jun 2006 14:50:33 +0000 (14:50 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 7 Jun 2006 14:50:33 +0000 (14:50 +0000)
required:
1) added <para> wrappers where missing
2) added titles to tables
3) removed empty <thead> elements
Point (3) make yelp now shows rules in tables used for syntax references. IMO
this not a good reason to have empty <thead> elements, since they violates the
docbook DTDs. Either yelp should be fixed to not ignore frame/rowsep/colsep
attributes (as it currently does) or we need to find a different markup for
displaying EBNF like grammars.

helm/software/matita/help/C/sec_commands.xml
helm/software/matita/help/C/sec_gettingstarted.xml
helm/software/matita/help/C/sec_intro.xml
helm/software/matita/help/C/sec_tacticals.xml
helm/software/matita/help/C/sec_terms.xml
helm/software/matita/help/C/sec_usernotation.xml

index b1bada0fddb9a06c348d8739c3ff639750155fc7..b4a6c8007679700dc27686e6a1b5dbf8064acb79 100644 (file)
@@ -2,6 +2,11 @@
 <!-- ============ Commands ====================== -->
 <chapter id="sec_commands">
  <title>Other commands</title>
- &TODO;
+ <sect1>
+   <title>Introduction</title>
+   <para>
+     &TODO;
+   </para>
+ </sect1>
 </chapter>
 
index 886603ab2d3facc60b06691f1423a93ff3eb3945..5f9dda35a829d1a6ba7fc86093841f1740de8fe6 100644 (file)
 
   <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>
      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>
    <sect2 id="developments">
    <title>How to use developments</title>
-   &TODO;
-   </sect2>
-   &TODO;
-  </sect1>
+   <para>   &TODO;</para>
+ </sect2>
+ </sect1>
 </chapter>
 
index a29b4960d1dede420648f00e6eb14720865b2ff5..773bda24ca7f86fe0e0cba580a3e5f6e103d6b98 100644 (file)
@@ -5,43 +5,44 @@
   <title>Introduction</title>
   <sect1 id="Features">
     <title>Features</title>
-
-    <para>
-      <application>Matita</application> is an interactive theorem prover
+    <para><application>Matita</application> is an interactive theorem prover
       (or proof assistant) with the following characteristics:</para>
-
     <itemizedlist>
-     <listitem>It is based on a variant of the Calculus of (co)Inductive
-      Constructions (CIC). CIC is also the logic of the Coq proof assistant.
-     </listitem>
-     <listitem>It adopts a procedural proof language, but it has a new
-      set of small step tacticals that improve proof structuring and debugging.
-     </listitem>
-     <listitem>It has a stand-alone graphical user interface (GUI) inspired by
-      CtCoq/Proof General. The GUI is implemented according to the state
-      of the art. In particular:
-      <itemizedlist>
-       <listitem>It is based and fully integrated with Gtk/Gnome.</listitem>
-       <listitem>An on-line help can be browsed via the Gnome documentation
-        browser.</listitem>
-       <listitem>Mathematical formulae are rendered in two dimensional
-        notation via MathML and Unicode.</listitem>
-      </itemizedlist>
-     </listitem>
-     <listitem>It integrates advanced browsing and searching procedures.
-     </listitem>
-     <listitem>It allows the use of the typical ambiguous mathematical notation
-      by means of a disambiguating parser.
-     </listitem>
-     <listitem>It is compatible with the library of Coq (definitions and
-      proof objects).
-     </listitem>
+      <listitem>
+        <para>It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant.</para>
+      </listitem>
+      <listitem>
+        <para>It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging.</para>
+      </listitem>
+      <listitem>
+        <para>It has a stand-alone graphical user interface (GUI) inspired by
+CtCoq/Proof General. The GUI is implemented according to the state
+of the art. In particular:</para>
+        <itemizedlist>
+          <listitem>
+            <para>It is based and fully integrated with Gtk/Gnome.</para>
+          </listitem>
+          <listitem>
+            <para>An on-line help can be browsed via the Gnome documentation browser.</para>
+          </listitem>
+          <listitem>
+            <para>Mathematical formulae are rendered in two dimensional notation via MathML and Unicode.</para>
+          </listitem>
+        </itemizedlist>
+      </listitem>
+      <listitem>
+        <para>It integrates advanced browsing and searching procedures.</para>
+      </listitem>
+      <listitem>
+        <para>It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser.</para>
+      </listitem>
+      <listitem>
+        <para>It is compatible with the library of Coq (definitions and proof objects).</para>
+      </listitem>
     </itemizedlist>
   </sect1>
-
   <sect1 id="WrtCoq">
     <title>Matita vs Coq</title>
-
     <para>
       The system shares a common look&amp;feel with the Coq proof assistant
       and its graphical user interface. The two systems have the same logic,
       From the user point of view the main lacking features
       with respect to Coq are:
     </para>
-
     <itemizedlist>
-     <listitem>proof extraction;</listitem>
-     <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>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>
+      <listitem>
+        <para>proof extraction;</para>
+      </listitem>
+      <listitem>
+        <para>an extensible language of tactics;</para>
+      </listitem>
+      <listitem>
+        <para>automatic implicit arguments;</para>
+      </listitem>
+      <listitem>
+        <para>several ad-hoc decision procedures;</para>
+      </listitem>
+      <listitem>
+        <para>several rarely used variants for most of the tactics;</para>
+      </listitem>
+      <listitem>
+        <para>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.</para>
+      </listitem>
     </itemizedlist>
-
     <para>
       Still from the user point of view, the main differences with respect
       to Coq are:
     </para>
-
     <itemizedlist>
-     <listitem>the language of tacticals that allows execution of partial
-      tactical application;</listitem>
-     <listitem>the unification of the concept of metavariable and existential
-      variable;</listitem>
-     <listitem>terms with subterms that cannot be inferred are always allowed
-      as arguments of tactics or other commands;</listitem>
-     <listitem>ambiguous terms are disambiguated by direct interaction
-      with the user;</listitem>
-     <listitem>theorems and definitions in the library are always accessible
-      without needing to require/include them; right now, only notation needs
-      to be included to become active, but we plan to remove this limitation.</listitem>
+      <listitem>
+        <para>the language of tacticals that allows execution of partial tactical application;</para>
+      </listitem>
+      <listitem>
+        <para>the unification of the concept of metavariable and existential variable;</para>
+      </listitem>
+      <listitem>
+        <para>terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands;</para>
+      </listitem>
+      <listitem>
+        <para>ambiguous terms are disambiguated by direct interaction with the user;</para>
+      </listitem>
+      <listitem>
+        <para>theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation.</para>
+      </listitem>
     </itemizedlist>
-
   </sect1>
 </chapter>
index 870feed7c510f755ebe99ed066fe86d68b975656..ea863605fb1db802ee410daf935c7a06d5f20a8d 100644 (file)
@@ -2,6 +2,11 @@
 <!-- ============ Tacticals ====================== -->
 <chapter id="sec_tacticals">
  <title>Tacticals</title>
- &TODO;
+ <sect1>
+   <title>Introduction</title>
+   <para>
+     &TODO;
+   </para>
+ </sect1>
 </chapter>
 
index 6d359a7acbb57cae135060e8e690c4ea1d911b44..fbf8dd4ef9cb614c7dfb52eb4c2fa80e1ab210b2 100644 (file)
@@ -5,62 +5,67 @@
   <title>Syntax</title>
   <para>To describe syntax in this manual we use the following conventions:</para>
   <orderedlist>
-   <listitem>Non terminal symbols are emphasized and have a link to their definition. E.g.: &term;</listitem>
-   <listitem>Terminal symbols are in bold. E.g.: <emphasis role="bold">theorem</emphasis></listitem>
-   <listitem>Optional sequences of elements are put in square brackets.
-    E.g.: [<emphasis role="bold">in</emphasis> &term;]</listitem>
-   <listitem>Alternatives are put in square brakets and they are separated
-    by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</listitem>
-   <listitem>Repetition of sequences of elements are given by putting the
+    <listitem><para>Non terminal symbols are emphasized and have a link to their
+       definition. E.g.: &term;</para></listitem>
+    <listitem><para>Terminal symbols are in bold. E.g.:
+       <emphasis role="bold">theorem</emphasis></para></listitem>
+    <listitem><para>Optional sequences of elements are put in square brackets.
+       E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
+    <listitem><para>Alternatives are put in square brakets and they are
+       separated by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</para></listitem>
+    <listitem><para>Repetition of sequences of elements are given by putting the
     first sequence in square brackets, that are followed by three dots.
-    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</listitem>
+    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
   </orderedlist>
   <sect1 id="terms_and_co">
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="id">&id;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="nat">&nat;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup cols="4">
-     <thead />
-    <tbody>
-     <row>
-      <entry id="uri">&uri;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
+  <para>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>id</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="id">&id;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>nat</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="nat">&nat;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>uri</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="uri">&uri;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+  </para>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
-  <table>
+  <para>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Terms</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="term">&term;</entry>
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Simple terms</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="sterm">&sterm;</entry>
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Arguments</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="args">&args;</entry>
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Miscellaneous arguments</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="args2">&args2;</entry>
    </tgroup>
   </table>
 
-  <table>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Pattern matching</title>
     <tgroup cols="4">
-     <thead />
     <tbody>
      <row>
       <entry id="match_pattern">&match_pattern;</entry>
     </tbody>
    </tgroup>
   </table>
+  </para>
 
   </sect2>
   </sect1>
index 92698f824e31b155c8e0d6644d6ac21c4ad311b8..dd1362d0200aa8cd64630b5428439e2db161e1ed 100644 (file)
@@ -2,6 +2,11 @@
 <!-- ============ User Notation ====================== -->
 <chapter id="sec_usernotation">
  <title>Extending the syntax</title>
- &TODO;
+ <sect1>
+   <title>Introduction</title>
+   <para>
+     &TODO;
+   </para>
+ </sect1>
 </chapter>