New: on-line help for declarative tactics (first version).

diff --git a/helm/software/matita/help/C/Makefile b/helm/software/matita/help/C/Makefile
index e85ad9a99608d4671e01cd9472f9737bdf1e9cb8..2ca1a16b1034f5dc5a9de11281a1f2d956ec62b0 100644 (file)
--- a/helm/software/matita/help/C/Makefile
+++ b/helm/software/matita/help/C/Makefile
@@ -14,9 +14,12 @@ DESTDIR = /usr/local/share/doc/matita/
 
 all: quickref
 
-quickref: tactic_quickref.xml
-tactic_quickref.xml: xsl/tactic_quickref.xsl sec_tactics.xml
-       $(XSLTPROC) $< matita.xml > tactic_quickref.xml
+quickref: tactics_quickref.xml declarative_tactics_quickref.xml
+
+tactics_quickref.xml: xsl/tactic_quickref.xsl sec_tactics.xml
+       $(XSLTPROC) --param declarative "''" $< matita.xml > tactics_quickref.xml
+declarative_tactics_quickref.xml: xsl/tactic_quickref.xsl sec_declarative_tactics.xml
+       $(XSLTPROC) --param declarative "'declarative_'" $< matita.xml > declarative_tactics_quickref.xml
 
 # one of: "fop", "pdflatex"
 PDF_METHOD=pdflatex
@@ -40,7 +43,7 @@ test:
 .PHONY: html
 html: html-stamp
 html-stamp: $(MAIN) $(DEPS) $(XHTML_XSL)
-       xsltproc $(XHTML_XSL) $<
+       $(XSLTPROC) $(XHTML_XSL) $<
        touch $@
 
 # TXTs generation
@@ -61,13 +64,13 @@ pdf-stamp: $(patsubst %.xml,%.pdf,$(MAIN))
        touch $@
 
 %.fo: %.xml
-       xsltproc $(FO_XSL) $< | xmllint --format - > $@
+       $(XSLTPROC) $(FO_XSL) $< | xmllint --format - > $@
 ifeq ($(TEX_METHOD),docbook2tex)
 %.tex: %.xml $(DEPS)
        docbook2tex $<
 else ifeq ($(TEX_METHOD),xsl)
 %.tex: %.xml $(TEX_XSL) $(DEPS)
-       xsltproc $(TEX_XSL) $< > $@
+       $(XSLTPROC) $(TEX_XSL) $< > $@
 endif
 
 ifeq ($(PDF_METHOD),fop)

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index bb281ac677b9f076b90acef045e368a6aea601f6..e20e17ad8db99f8527b184ff0a3254d0649519b0 100644 (file)
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -10,10 +10,12 @@
   <!ENTITY terms SYSTEM "sec_terms.xml">
   <!ENTITY tacticals SYSTEM "sec_tacticals.xml">
   <!ENTITY tactics SYSTEM "sec_tactics.xml">
+  <!ENTITY declarative_tactics SYSTEM "sec_declarative_tactics.xml">
   <!ENTITY othercommands SYSTEM "sec_commands.xml">
   <!ENTITY usernotation SYSTEM "sec_usernotation.xml">
 
-  <!ENTITY tacticref SYSTEM "tactic_quickref.xml">
+  <!ENTITY tacticref SYSTEM "tactics_quickref.xml">
+  <!ENTITY declarativetacticref SYSTEM "declarative_tactics_quickref.xml">
 
   <!ENTITY manrevision "1&alpha;">
   <!ENTITY date "12/07/2006">
@@ -127,6 +129,7 @@
 &usernotation;
 &tacticals;
 &tactics;
+&declarative_tactics;
 &othercommands;
 &license;
 

diff --git a/helm/software/matita/help/C/sec_declarative_tactics.xml b/helm/software/matita/help/C/sec_declarative_tactics.xml
new file mode 100644 (file)
index 0000000..1bbbd57
--- /dev/null
+++ b/helm/software/matita/help/C/sec_declarative_tactics.xml
@@ -0,0 +1,471 @@
+<!-- ================= Tactics ========================= -->
+<chapter id="sec_declarative_tactics">
+  <title> Tactics Declarative</title>
+
+  <sect1
+  id="declarative_tactics_quickref">
+    <title>Quick reference card</title>
+    <para>
+      &declarativetacticref;
+    </para>
+  </sect1>
+
+  
+  <sect1 id="tac_assume">
+    <title>assume</title>
+    <titleabbrev>assume</titleabbrev>
+    <para><userinput>assume x : t</userinput></para>
+  <para>
+    <variablelist>
+      <varlistentry role="tactic.synopsis">
+       <term>Synopsis:</term>
+       <listitem>
+         <para><emphasis role="bold">assume</emphasis> &id; <emphasis role="bold"> : </emphasis> &sterm;</para>
+       </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>Pre-conditions:</term>
+       <listitem>
+         <para>The conclusion of the current proof must be
+          <command>∀x:T.P</command> or
+          <command>T→P</command> where <command>T</command> is
+          a data type (i.e. <command>T</command> has type
+          <command>Set</command> or <command>Type</command>).</para>
+       </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>Action:</term>
+       <listitem>
+         <para>It adds to the context of the current sequent to prove a new
+          declaration <command>x : T </command>. The new conclusion becomes
+          <command>P</command>.</para>
+       </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>New sequents to prove:</term>
+       <listitem>
+         <para>None.</para>
+       </listitem>
+      </varlistentry>
+    </variablelist>
+   </para>
+  </sect1>
+
+  <sect1 id="tac_suppose">
+    <title>suppose</title>
+    <titleabbrev>suppose</titleabbrev>
+    <para><userinput>suppose t(x) </userinput></para>
+  <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+        <listitem>
+          <para><emphasis role="bold">suppose</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; 
+            <emphasis role="bold">) </emphasis> [ that is equivalent to  &term; ]</para>
+        </listitem>
+       </varlistentry>
+      <varlistentry>
+         <term>Pre-condition:</term>
+        <listitem>
+          <para> Da Fare </para>
+        </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>Action:</term>
+         <listitem>
+           <para> Da Fare </para>
+         </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>New sequents to prove:</term>
+        <listitem>
+            <para>None.</para>
+        </listitem>
+      </varlistentry>
+    </variablelist>
+   </para>
+  </sect1>
+
+ <sect1 id="tac_bydone">
+   <title>by done</title>
+   <titleabbrev>by done</titleabbrev>
+   <para><userinput>by [ t | _ ] done</userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+        <listitem>
+          <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold"> done </emphasis></para>
+        </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Pre-condition:</term>
+        <listitem>
+          <para>The term can be omitted with a "_", the running term will come found automatically. </para>
+        </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+          <listitem> 
+            <para>It closes the current sequent by applying <command>t</command>, taht it can be one under proof or the main proof.</para>
+          </listitem>
+       </varlistentry>
+       <varlistentry>
+           <term>New sequents to prove:</term>
+           <listitem>
+               <para>None.</para>
+           </listitem>
+       </varlistentry>
+   </variablelist>
+     </para>
+  </sect1>
+
+  <sect1 id="tac_weneedtoprove">
+    <title> we need to prove</title>
+    <titleabbrev>we need to prove</titleabbrev>
+    <para><userinput>we need to prove t [(id)] [or equivalent t]</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+            <para><emphasis role="bold">we need to prove</emphasis> &term; </para>
+         </listitem>
+       </varlistentry>
+        <varlistentry>
+          <term>Pre-condition:</term>
+         <listitem>
+           <para> Da Fare </para>
+         </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+           <listitem>
+             <para> Da Fare </para>
+           </listitem>
+        </varlistentry>
+        <varlistentry>
+           <term>New sequents to prove:</term>
+          <listitem>
+            <para>None.</para>
+          </listitem>
+       </varlistentry>     
+     </variablelist>
+    </para>
+  </sect1>
+
+  <sect1 id="tac_weproceedbyinduction">
+    <title> we proceed by induction</title>
+    <titleabbrev>we proceed by induction</titleabbrev>
+    <para><userinput>we proceed by induction on t to prove th</userinput></para>        
+    <para>
+      <variablelist>
+        <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">we proceed by induction on</emphasis> &term; <emphasis role="bold"> to prove </emphasis> &term; </para>
+         </listitem>
+       </varlistentry>
+        <varlistentry>
+         <term>Pre-condition:</term>
+         <listitem>
+           <para><command>t</command> must inhabit an inductive type and <command>th</command> must be an elimination principle for that inductive type.</para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+           <listitem>
+             <para>It proceed on the values of <command>t</command>.</para>
+           </listitem>
+       </varlistentry>
+        <varlistentry>
+            <term>New sequents to prove:</term>
+            <listitem>
+               <para>It opens one new sequent to demonstrate.</para>
+            </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
+  </sect1>
+
+  <sect1 id="tac_weproceedbycases">
+    <title>we proceed by cases</title>
+      <titleabbrev>we proceed by cases</titleabbrev>
+      <para><userinput>we proceed by cases on t to prove t</userinput></para>
+      <para>
+        <variablelist>
+         <varlistentry role="tactic.synopsis">
+           <term>Synopsis:</term>
+           <listitem>
+             <para><emphasis role="bold">we proceed by cases on </emphasis> &term; <emphasis role="bold">to prove</emphasis> &term; </para>
+            </listitem>
+          </varlistentry>
+         <varlistentry>
+           <term>Pre-condition:</term>
+           <listitem>
+             <para> Da Fare </para>
+           </listitem>
+         </varlistentry>
+         <varlistentry>
+           <term>Action:</term>
+             <listitem>
+               <para> Da Fare </para>
+              </listitem>
+         </varlistentry>
+          <varlistentry>
+            <term>New sequents to prove:</term>
+           <listitem>
+              <para>None.</para>
+           </listitem>
+         </varlistentry>
+         </variablelist>
+       </para>
+    </sect1>
+
+    <sect1 id="tac_byinduction">
+      <title>by induction</title>
+      <titleabbrev>by induction</titleabbrev>
+      <para><userinput>by induction hypothesis we know t (id)</userinput></para>
+      <para>
+        <variablelist>
+         <varlistentry role="tactic.synopsis">
+           <term>Synopsis:</term>
+           <listitem>
+             <para><emphasis role="bold">by induction hypothesis we know</emphasis> &term; <emphasis role="bold"> (</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+           </listitem>
+         </varlistentry>
+         <varlistentry>
+           <term>Pre-condition:</term>
+           <listitem>
+             <para> Da Fare </para>
+           </listitem>
+         </varlistentry>
+         <varlistentry>
+           <term>Action:</term>
+             <listitem>
+               <para> Da Fare </para>
+             </listitem>
+         </varlistentry>
+          <varlistentry>
+             <term>New sequents to prove:</term>
+                <listitem>
+                <para>None.</para>
+                </listitem>
+         </varlistentry>
+         </variablelist>
+      </para>
+    </sect1>  
+
+   <sect1 id="tac_thesisbecomes">
+     <title>thesis becomes</title>
+     <titleabbrev>thesis becomes</titleabbrev>
+     <para><userinput>the thesis becomes t</userinput></para>
+     <para>
+        <variablelist>
+          <varlistentry role="tactic.synopsis">
+            <term>Synopsis:</term>
+            <listitem>
+              <para><emphasis role ="bold">the thesis becomes</emphasis> &sterm; </para>
+            </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>Pre-condition:</term>
+            <listitem>
+              <para>Each subterm must be convertible with the term <command>t</command> disambiguate in the context of the matched subterm.</para>
+            </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>Action:</term>
+            <listitem>
+              <para>It replaces the subterm of the current sequent with the new term</para>
+            </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>New sequence to prove:</term>
+            <listitem>
+              <para>None.</para>
+            </listitem>
+          </varlistentry>
+        </variablelist>
+       </para>
+   </sect1>
+   
+   <sect1 id="tac_case">
+     <title>case</title>
+     <titleabbrev>case</titleabbrev>
+     <para><userinput>case id (id:t)list</userinput></para>
+     <para>
+       <variablelist>
+         <varlistentry role="tactic.synopsis">
+          <term>Synopsis:</term>
+          <listitem>
+            <para><emphasis role="bold">case</emphasis> &id; <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">)</emphasis></para>
+          </listitem>
+        </varlistentry>
+         <varlistentry>
+            <term>Pre-condition:</term>
+           <listitem>
+               <para> Da Fare </para>
+           </listitem>
+        </varlistentry>
+         <varlistentry>
+            <term>Action:</term>
+            <listitem>
+              <para> Da Fare </para>
+            </listitem>
+         </varlistentry>
+         <varlistentry>
+           <term>New sequents to prove:</term>
+           <listitem>
+               <para>Da Fare</para>
+           </listitem>
+         </varlistentry>
+       </variablelist>
+     </para>
+  </sect1> 
+
+  <sect1 id="tac_obtain">
+    <title>obtain</title>
+    <titleabbrev>obtain</titleabbrev>
+    <para><userinput>obtain t=t by [t|_]</userinput></para>
+    <para>
+      <variablelist>
+         <varlistentry role="tactic.synopsis">
+          <term>Synopsis:</term>
+          <listitem>
+            <para><emphasis role="bold">obtain</emphasis> &term; <emphasis role="bold">=</emphasis> &term; <emphasis role="bold">by</emphasis> [ &term; | _ ]</para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Pre-condition:</term>
+            <listitem>
+              <para> Da Fare </para>
+            </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem>
+             <para> Da Fare </para>
+           </listitem>
+         </varlistentry>
+        <varlistentry>
+          <term>New sequence to prove:</term>
+            <listitem>
+               <para> Da Fare </para>
+            </listitem>
+        </varlistentry>
+       </variablelist>
+     </para>
+   </sect1>
+
+ <sect1 id="tac_bytermweproved">
+   <title>by term we proved</title>
+     <titleabbrev>by term we proved</titleabbrev>
+     <para><userinput>by th we proved t [""|(id)]</userinput></para>
+     <para>
+       <variablelist>
+         <varlistentry role="tactic.synopsis">
+          <term>Synopsis:</term>
+          <listitem>
+            <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">we proved</emphasis> &term; 
+                  <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+           </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>Pre-condition:</term>
+            <listitem>
+              <para><command>th</command>must have type <command>Prop</command>.
+                    <command>id</command>can to be omitted with null</para>
+            </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>Action:</term>
+            <listitem>
+              <para>It closes the current sequent by applying<command>th</command> to <command>t</command>.</para>
+            </listitem>
+          </varlistentry>
+          <varlistentry>
+            <term>New sequence to prove:</term>
+            <listitem>
+              <para> Da fare </para>
+            </listitem>
+          </varlistentry>
+        </variablelist>
+       </para>
+    </sect1>
+
+  <sect1 id="tac_exitselim">
+    <title>exits elim</title>
+    <titleabbrev>exits elim</titleabbrev>
+    <para><userinput>by t let id:t such that t (id)</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">let</emphasis> &id; 
+                   <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">such that</emphasis> &term; 
+                    <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
+          </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Pre-condition:</term>
+         <listitem>
+           <para><command>t</command> must be an inductive type,existential and 
+              <command>t (id)</command> must be an elimanation priciple for that inductive type.
+           </para>
+         </listitem>  
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>it proceeds on <command>t</command> to the elimination of the existential one </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>New sequence to prove:</term>
+         <listitem>
+           <para>It opens one new sequent. The names of the new hypotheses are picked by<command>t (id)</command> </para>
+         </listitem>
+       </varlistentry>
+     </variablelist>
+    </para>
+  </sect1>
+
+  <sect1 id="tac_andelim">
+    <title>and elim</title>
+    <titleabbrev>and elim</titleabbrev>
+    <para><userinput>by t we have t (id) and t (id)</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry role="tactic_synopsis">
+         <term>Synopsis:</term>
+         <listitem>
+           <para><emphasis role="bold">by</emphasis> &term; <emphasis role="bold">we have</emphasis> &term; 
+                   <emphasis role="bold">( </emphasis> &id; <emphasis role="bold"> ) and </emphasis> &term; 
+                     <emphasis role="bold"> ( </emphasis> &id; <emphasis role="bold">)</emphasis></para>
+          </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Pre-condition:</term>
+         <listitem>
+           <para><command>t</command> must be an logical type,type and  </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+         <listitem>
+           <para>It proceeds on the values of <command>t</command>, according to the elimination principle </para>
+         </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>New sequence to prove:</term>
+         <listitem>
+            <para>It opens one new sequent, the names of the new hypotheses are picked by <command>t(id) and t(id)</command> </para>
+          </listitem>
+       </varlistentry>
+      </variablelist>
+    </para>
+  </sect1>
+
+</chapter>

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 5f682eb83ccdb6a67ee68199c4565021cd40d412..2e5f406c9252f0a6719aa322e0906a112e48cdac 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -426,6 +426,7 @@
   <sect2 id="letrec">
     <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
     <titleabbrev>&TODO;</titleabbrev>
+    <para>&TODO</para>
   </sect2>
   <sect2 id="inductive">
     <title>[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…

diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index 1549d3794a3b9e298afeca205f9e9f44ecbb7fb4..e1ff24b3803d82e41e90f20b87873659d4d8c129 100644 (file)
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -1,303 +1,6 @@
 <table frame="topbot" rowsep="0" colsep="0" role="grammar">
-  <title>tactics</title>
+  <title>tacticssec__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>…]
-           </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>…]
-           </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_destruct"><emphasis role="bold">destruct</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_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>] 
-            <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> 
-            [<emphasis role="bold">to</emphasis>
-             <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
-             [<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>]
-           </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_subst">
-            <emphasis role="bold">subst</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>
+    <tbody/>
   </tgroup>
 </table>

diff --git a/helm/software/matita/help/C/xsl/tactic_quickref.xsl b/helm/software/matita/help/C/xsl/tactic_quickref.xsl
index 42e435740e719c59253bb75563be8d3671ddf44c..3a46261e0783937c4841fb519cd6ead5f44786e8 100644 (file)
--- a/helm/software/matita/help/C/xsl/tactic_quickref.xsl
+++ b/helm/software/matita/help/C/xsl/tactic_quickref.xsl
@@ -7,12 +7,14 @@
     omit-xml-declaration="yes"
     />
 
+  <xsl:param name="declarative" value=""/>
+
   <xsl:template match="/">
     <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:apply-templates select="//chapter[@id=concat('sec_',$declarative,'tactics')]//varlistentry[@role='tactic.synopsis']">
         <xsl:sort select="ancestor::sect1/title" />
        </xsl:apply-templates>
       </tbody>
@@ -30,7 +32,7 @@
       <entry>
        <xsl:choose>
         <xsl:when test="position()=1">
-         <xsl:attribute name="id">grammar.tactic</xsl:attribute>
+         <xsl:attribute name="id">grammar.<xsl:value-of select="$declarative"/>tactic</xsl:attribute>
          <xsl:text disable-output-escaping='yes'>&amp;tactic;</xsl:text>
         </xsl:when>
        </xsl:choose>