better description of declarative tactics

[helm.git] / helm / software / matita / help / C / declarative_tactics_quickref.xml

diff --git a/helm/software/matita/help/C/declarative_tactics_quickref.xml b/helm/software/matita/help/C/declarative_tactics_quickref.xml
index 2d09883af5b7647b6218fcf0788a5e6ceb0652ac..002a7a376bbd4037391b17975ee1ab4e7a01b348 100644 (file)
--- a/helm/software/matita/help/C/declarative_tactics_quickref.xml
+++ b/helm/software/matita/help/C/declarative_tactics_quickref.xml
@@ -5,66 +5,70 @@
       <row>
         <entry id="grammar.declarative_tactic">&tactic;</entry>
         <entry>::=</entry>
-        <entry><emphasis role="bold">we need to prove</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
+        <entry><link linkend="tac_assume"><emphasis role="bold">assume</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><emphasis role="bold">we proceed by induction on</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> to prove </emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
+        <entry><link linkend="tac_by induction hypothesis we know"><emphasis role="bold">by induction hypothesis we know</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_assume"><emphasis role="bold">assume</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold"> : </emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry><link linkend="tac_case"><emphasis role="bold">case</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>  <emphasis role="bold">)</emphasis>] … </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">by</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> done </emphasis></entry>
+        <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_done"><emphasis role="bold">done</emphasis></link></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">by induction hypothesis we know</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
+        <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <emphasis role="bold">let</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> 
+                   <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">such that</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> 
+                    <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">by</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">we proved</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> 
-                  <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
+        <entry>[<link linkend="tac_obtain"><emphasis role="bold">obtain</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> | <emphasis role="bold">conclude</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>] <emphasis role="bold">=</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> [<emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis> | <emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">using once</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_case"><emphasis role="bold">case</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">)</emphasis></entry>
+        <entry><link linkend="tac_suppose"><emphasis role="bold">suppose</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> 
+            <emphasis role="bold">) </emphasis> [ <emphasis role="bold">that is equivalent to</emphasis>  <emphasis><link linkend="grammar.term">term</link></emphasis> ]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">by</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">let</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> 
-                   <emphasis role="bold">:</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">such that</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> 
-                    <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">)</emphasis></entry>
+        <entry><link linkend="tac_the thesis becomes"><emphasis role="bold">the thesis becomes</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry>[<emphasis role="bold">obtain</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> | <emphasis role="bold">conclude</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>] <emphasis role="bold">=</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">by</emphasis> [ <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">_</emphasis> [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">)</emphasis>]] [<emphasis role="bold">done</emphasis>]</entry>
+        <entry><link linkend="tac_we need to prove"><emphasis role="bold">we need to prove</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis>
+        [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>
+        <emphasis role="bold">)</emphasis>]
+        [ <emphasis role="bold">or equivalently</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis>]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_suppose"><emphasis role="bold">suppose</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> (</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> 
-            <emphasis role="bold">) </emphasis> [ that is equivalent to  <emphasis><link linkend="grammar.term">term</link></emphasis> ]</entry>
+        <entry><link linkend="tac_we proceed by cases on"><emphasis role="bold">we proceed by cases on</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">to prove</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">the thesis becomes</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> </entry>
+        <entry><link linkend="tac_we proceed by induction on"><emphasis role="bold">we proceed by induction on</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold"> to prove </emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">we proceed by cases on </emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis role="bold">to prove</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> </entry>
+        <entry><emphasis><link linkend="grammar.justification">justification</link></emphasis> <link linkend="tac_we proved"><emphasis role="bold">we proved</emphasis></link> <emphasis><link linkend="grammar.term">term</link></emphasis> 
+         <emphasis role="bold">(</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> 
+         <emphasis role="bold">)</emphasis></entry>
       </row>
     </tbody>
   </tgroup>