Documentation of tinycals started.

diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml
index a20663feca12417527b1f73c1dc34a1eb9103e1a..98d6489f335ff6a40c44a30bd0f847533aa3e81a 100644 (file)
--- a/matita/help/C/matita.xml
+++ b/matita/help/C/matita.xml
@@ -8,8 +8,8 @@
   <!ENTITY gettingstarted SYSTEM "sec_gettingstarted.xml">
   <!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 tactics SYSTEM "sec_tactics.xml">
   <!ENTITY othercommands SYSTEM "sec_commands.xml">
   <!ENTITY usernotation SYSTEM "sec_usernotation.xml">
 
@@ -42,6 +42,10 @@
   <!ENTITY pattern "<emphasis><link linkend='grammar.pattern'>pattern</link></emphasis>">
   <!ENTITY reduction-kind "<emphasis><link linkend='grammar.reduction-kind'>reduction-kind</link></emphasis>">
   <!ENTITY path "<emphasis><link linkend='grammar.path'>path</link></emphasis>">
+  <!ENTITY proofscript "<emphasis><link linkend='grammar.proofscript'>proof-script</link></emphasis>">
+  <!ENTITY proofstep "<emphasis><link linkend='grammar.proofstep'>proof-step</link></emphasis>">
+  <!ENTITY tactic "<emphasis><link linkend='grammar.tactic'>tactic</link></emphasis>">
+  <!ENTITY LCFtactical "<emphasis><link linkend='grammar.LCFtactical'>LCF-tactical</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
@@ -118,8 +122,8 @@
 &gettingstarted;
 &terms;
 &usernotation;
-&tactics;
 &tacticals;
+&tactics;
 &othercommands;
 &license;
 

diff --git a/matita/help/C/sec_commands.xml b/matita/help/C/sec_commands.xml
index b4a6c8007679700dc27686e6a1b5dbf8064acb79..243960cf9c402e053a27f2071e1eb287b675c881 100644 (file)
--- a/matita/help/C/sec_commands.xml
+++ b/matita/help/C/sec_commands.xml
@@ -8,5 +8,9 @@
      &TODO;
    </para>
  </sect1>
+ <sect1 id="command_qed">
+   <title>Qed</title>
+   <para>&TODO;</para>
+ </sect1>
 </chapter>
 

diff --git a/matita/help/C/sec_tacticals.xml b/matita/help/C/sec_tacticals.xml
index ea863605fb1db802ee410daf935c7a06d5f20a8d..981914c9fc073fe8b2ef4eb7dbc296ec097f590f 100644 (file)
--- a/matita/help/C/sec_tacticals.xml
+++ b/matita/help/C/sec_tacticals.xml
@@ -3,10 +3,178 @@
 <chapter id="sec_tacticals">
  <title>Tacticals</title>
  <sect1>
-   <title>Introduction</title>
+   <title>Interactive proofs and definitions</title>
    <para>
-     &TODO;
+    An interactive definition is started by giving a
+    <link linkend="definition">definition</link> command omitting
+    the definiens.
+    An interactive proof is started by using one of the
+    <link linkend="proofs">proof commands</link> omitting
+    an explicit proof term.
    </para>
+   <para>An interactive proof or definition can and must be terminated by
+    a <link linkend="command_qed">qed</link> command when no more sequents are
+    left to prove. Between the command that starts the interactive session and
+    the qed command the user must provide a procedural proof script made
+    of <link linkend="sec_tactics">tactics</link> structured by means of
+    <link linkend="tacticals">tacticals</link>.</para>
+   <para>In the tradition of the LCF system, tacticals can be considered
+    higher order tactics. Their syntax is structured and they are executed
+    atomically. On the contrary, in Matita the syntax of several tacticals is
+    destructured into a sequence of tokens and tactics in such a way that is
+    is possible to stop execution after every single token or tactic.
+    The original semantics is preserved: the execution of the whole sequence
+    yields the result expected by the original LCF-like tactical.</para>
+ </sect1>
+ <sect1 id="tacticals">
+  <title>Tacticals</title>
+   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+     <title>proof script</title>
+     <tgroup cols="4">
+     <tbody>
+      <row>
+       <entry id="grammar.proofscript">&proofscript;</entry>
+       <entry>::=</entry>
+       <entry>&proofstep; [&proofstep;]…</entry>
+      </row>
+     </tbody>
+    </tgroup>
+   </table>
+   <para>Every proof step can be immediately executed.</para>
+   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+     <title>proof steps</title>
+     <tgroup cols="4">
+     <tbody>
+      <row>
+       <entry id="grammar.proofstep">&proofstep;</entry>
+       <entry>::=</entry>
+       <entry>&LCFtactical;</entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">.</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">;</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">[</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">|</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry>&nat;[<emphasis role="bold">,</emphasis>&nat;]…<emphasis role="bold">:</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">*:</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">skip</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">]</emphasis></entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">focus</emphasis> &nat; [&nat;]…</entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">unfocus</emphasis></entry>
+      </row>
+     </tbody>
+    </tgroup>
+   </table>
+   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+     <title>tactics and LCF tacticals</title>
+     <tgroup cols="4">
+     <tbody>
+      <row>
+       <entry id="grammar.LCFtactical">&LCFtactical;</entry>
+       <entry>::=</entry>
+       <entry>&tactic;</entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry>&LCFtactical; <emphasis role="bold">;</emphasis> &LCFtactical;</entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry>&LCFtactical;
+        <emphasis role="bold">[</emphasis>
+        [&LCFtactical;]
+        [<emphasis role="bold">|</emphasis> &LCFtactical;]…
+        <emphasis role="bold">]</emphasis>
+       </entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">do</emphasis> &nat;
+        &LCFtactical; <emphasis role="bold">end</emphasis>
+       </entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">repeat</emphasis>
+        &LCFtactical; <emphasis role="bold">end</emphasis>
+       </entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry>
+        <emphasis role="bold">first [</emphasis>
+        [&LCFtactical;]
+        [<emphasis role="bold">|</emphasis> &LCFtactical;]…
+        <emphasis role="bold">]</emphasis>
+       </entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">try</emphasis> &LCFtactical;</entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry>
+        <emphasis role="bold">solve [</emphasis>
+        [&LCFtactical;]
+        [<emphasis role="bold">|</emphasis> &LCFtactical;]…
+        <emphasis role="bold">]</emphasis>
+       </entry>
+      </row>
+      <row>
+       <entry/>
+       <entry>|</entry>
+       <entry><emphasis role="bold">(</emphasis>&LCFtactical;<emphasis role="bold">)</emphasis></entry>
+      </row>
+     </tbody>
+    </tgroup>
+   </table>
+   <para>&TODO;</para>
  </sect1>
 </chapter>
 

diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml
index 58fd32afd506fb8fd67f87f80b9ddc3e0f2010a0..b41ae79eb22189e61e7c2bfb31248a5a9ad7d6e6 100644 (file)
--- a/matita/help/C/tactic_quickref.xml
+++ b/matita/help/C/tactic_quickref.xml
@@ -1,125 +1,184 @@
-<itemizedlist>
-  <listitem>
-    <para><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_assumption">
-        <emphasis role="bold">assumption</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">width=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>]</para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
+<table frame="topbot" rowsep="0" colsep="0" role="grammar">
+  <title>tactics</title>
+  <tgroup cols="3">
+    <tbody>
+      <row>
+        <entry id="grammar.tactic">&tactic;</entry>
+        <entry>::=</entry>
+        <entry><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_assumption">
+            <emphasis role="bold">assumption</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">width=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>]</entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
             <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
             <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
-           </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_contradiction">
-        <emphasis role="bold">contradiction</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
-  </listitem>
-  <listitem>
-    <para>
+           </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_contradiction">
+            <emphasis role="bold">contradiction</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
             <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
             [<emphasis role="bold">(</emphasis>
             <emphasis><link linkend="grammar.id">id</link></emphasis>…
             <emphasis role="bold">)</emphasis>]
             [<emphasis><link linkend="grammar.id">id</link></emphasis>] 
             [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
-           </para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_demodulate">
-        <emphasis role="bold">demodulate</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_elimType"><emphasis role="bold">elimType</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_exists">
-        <emphasis role="bold">exists</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_fail">
-        <emphasis role="bold">fail</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_fold"><emphasis role="bold">fold</emphasis></link> <emphasis><link linkend="grammar.reduction-kind">reduction-kind</link></emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_fourier">
-        <emphasis role="bold">fourier</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_id">
-        <emphasis role="bold">id</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_injection"><emphasis role="bold">injection</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
+           </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_demodulate">
+            <emphasis role="bold">demodulate</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_elimType"><emphasis role="bold">elimType</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_exists">
+            <emphasis role="bold">exists</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_fail">
+            <emphasis role="bold">fail</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_fold"><emphasis role="bold">fold</emphasis></link> <emphasis><link linkend="grammar.reduction-kind">reduction-kind</link></emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_fourier">
+            <emphasis role="bold">fourier</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_id">
+            <emphasis role="bold">id</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_injection"><emphasis role="bold">injection</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
             <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> 
             [<emphasis role="bold">linear</emphasis>]
             [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] 
@@ -129,78 +188,112 @@
              [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
             ] 
             [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
-           </para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_left">
-        <emphasis role="bold">left</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_letin"><emphasis role="bold">letin</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">≝</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_paramodulation"><emphasis role="bold">paramodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_reflexivity">
-        <emphasis role="bold">reflexivity</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_replace"><emphasis role="bold">replace</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_right">
-        <emphasis role="bold">right</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_ring">
-        <emphasis role="bold">ring</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_split">
-        <emphasis role="bold">split</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para>
-      <link linkend="tac_symmetry">
-        <emphasis role="bold">symmetry</emphasis>
-      </link>
-    </para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_unfold"><emphasis role="bold">unfold</emphasis></link> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-  <listitem>
-    <para><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
-  </listitem>
-</itemizedlist>
+           </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_left">
+            <emphasis role="bold">left</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_letin"><emphasis role="bold">letin</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">≝</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_paramodulation"><emphasis role="bold">paramodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_reflexivity">
+            <emphasis role="bold">reflexivity</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_replace"><emphasis role="bold">replace</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_right">
+            <emphasis role="bold">right</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_ring">
+            <emphasis role="bold">ring</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_split">
+            <emphasis role="bold">split</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_symmetry">
+            <emphasis role="bold">symmetry</emphasis>
+          </link>
+        </entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_unfold"><emphasis role="bold">unfold</emphasis></link> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+      </row>
+    </tbody>
+  </tgroup>
+</table>

diff --git a/matita/help/C/xsl/tactic_quickref.xsl b/matita/help/C/xsl/tactic_quickref.xsl
index fa9c034fcabbcdcf56c9fefa0bdbdf7f5474a8ab..42e435740e719c59253bb75563be8d3671ddf44c 100644 (file)
--- a/matita/help/C/xsl/tactic_quickref.xsl
+++ b/matita/help/C/xsl/tactic_quickref.xsl
@@ -8,11 +8,16 @@
     />
 
   <xsl:template match="/">
-    <itemizedlist>
-      <xsl:apply-templates select="//varlistentry[@role='tactic.synopsis']">
-       <xsl:sort select="ancestor::sect1/title" />
-      </xsl:apply-templates>
-    </itemizedlist>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>tactics</title>
+      <tgroup cols="3">
+      <tbody>
+       <xsl:apply-templates select="//varlistentry[@role='tactic.synopsis']">
+        <xsl:sort select="ancestor::sect1/title" />
+       </xsl:apply-templates>
+      </tbody>
+     </tgroup>
+    </table>
   </xsl:template>
 
   <xsl:template match="varlistentry">
@@ -21,8 +26,26 @@
       <xsl:value-of select="ancestor::sect1/title" />
     </xsl:variable>
 
-    <listitem>
-      <para>
+    <row>
+      <entry>
+       <xsl:choose>
+        <xsl:when test="position()=1">
+         <xsl:attribute name="id">grammar.tactic</xsl:attribute>
+         <xsl:text disable-output-escaping='yes'>&amp;tactic;</xsl:text>
+        </xsl:when>
+       </xsl:choose>
+      </entry>
+      <entry>
+       <xsl:choose>
+        <xsl:when test="position()=1">
+         <xsl:text>::=</xsl:text>
+        </xsl:when>
+        <xsl:otherwise>
+         <xsl:text>|</xsl:text>
+        </xsl:otherwise>
+       </xsl:choose>
+      </entry>
+      <entry>
        <xsl:for-each select="listitem/para/* | listitem/para/child::text()">
          <xsl:choose>
 
@@ -42,8 +65,8 @@
 
          </xsl:choose>
        </xsl:for-each>
-      </para>
-    </listitem>
+      </entry>
+    </row>
 
   </xsl:template>