X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Ftactic_quickref.xml;h=e44a53068e7bd6a17bcde0c95b23dca929c30e63;hb=f01ea391a615404b49aee832452bec33d3e595dd;hp=dd14d8a2685b15d99c9493b9bebeaf21a7de122a;hpb=f68f452173a5077c58f93587faad65fcced77223;p=helm.git

diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml
index dd14d8a26..e44a53068 100644
--- a/matita/help/C/tactic_quickref.xml
+++ b/matita/help/C/tactic_quickref.xml
@@ -1,121 +1,189 @@
-<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_applyS"><emphasis role="bold">applyS</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_demodulation"><emphasis role="bold">demodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></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>] 
@@ -125,78 +193,107 @@
 	      [<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_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>