From f63e9358746f82de0dd07d60bdf82fdc0fae2101 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 26 May 2008 16:33:07 +0000
Subject: [PATCH] better description of declarative tactics

---
 .../help/C/declarative_tactics_quickref.xml   |  36 +-
 helm/software/matita/help/C/matita.xml        |   3 +-
 .../matita/help/C/sec_declarative_tactics.xml | 599 ++++++++++--------
 helm/software/matita/help/C/sec_terms.xml     |  24 +-
 4 files changed, 368 insertions(+), 294 deletions(-)

diff --git a/helm/software/matita/help/C/declarative_tactics_quickref.xml b/helm/software/matita/help/C/declarative_tactics_quickref.xml
index 8aba5a08c..002a7a376 100644
--- 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><link linkend="grammar.autoparams">auto_params</link></emphasis> | <emphasis role="bold">exact</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.term">term</link></emphasis> | <emphasis role="bold">proof</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>
diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 1b4cba2aa..3f00c148f 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -17,7 +17,7 @@
   <!ENTITY tacticref SYSTEM "tactics_quickref.xml">
   <!ENTITY declarativetacticref SYSTEM "declarative_tactics_quickref.xml">
 
-  <!ENTITY manrevision "1&alpha;">
+  <!ENTITY manrevision SYSTEM "version.txt">
   <!ENTITY date "12/07/2006">
   <!ENTITY app "<application>Matita</application>">
   <!ENTITY appname "Matita">
@@ -53,6 +53,7 @@
   <!ENTITY qstring "<emphasis><link linkend='grammar.qstring'>qstring</link></emphasis>">
   <!ENTITY interpretation "<emphasis><link linkend='grammar.interpretation'>interpretation</link></emphasis>">
   <!ENTITY autoparams "<emphasis><link linkend='grammar.autoparams'>auto_params</link></emphasis>">
+  <!ENTITY justification "<emphasis><link linkend='grammar.justification'>justification</link></emphasis>">
   <!ENTITY simpleautoparam "<emphasis><link linkend='grammar.simpleautoparam'>simple_auto_param</link></emphasis>">
 ]>
 
diff --git a/helm/software/matita/help/C/sec_declarative_tactics.xml b/helm/software/matita/help/C/sec_declarative_tactics.xml
index cc6aeb61d..bc0b424e0 100644
--- a/helm/software/matita/help/C/sec_declarative_tactics.xml
+++ b/helm/software/matita/help/C/sec_declarative_tactics.xml
@@ -51,199 +51,28 @@
    </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> &TODO; </para>
-	 </listitem>
-      </varlistentry>
-      <varlistentry>
-        <term>Action:</term>
-	  <listitem>
-	    <para> &TODO; </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> &TODO; </para>
-	  </listitem>
-        </varlistentry>
-        <varlistentry>
-          <term>Action:</term>
-	    <listitem>
-	      <para> &TODO; </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> &TODO; </para>
-	    </listitem>
-	  </varlistentry>
-	  <varlistentry>
-	    <term>Action:</term>
-	      <listitem>
-	        <para> &TODO; </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>
+      <title>by induction hypothesis we know</title>
+      <titleabbrev>by induction hypothesis we know</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><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> &TODO; </para>
+        <para>To be used in a proof by induction to state the inductive
+          hypothesis.</para>
 	    </listitem>
 	  </varlistentry>
 	  <varlistentry>
 	    <term>Action:</term>
 	      <listitem>
-	        <para> &TODO; </para>
+	        <para> Introduces the inductive hypothesis. </para>
 	      </listitem>
 	  </varlistentry>
           <varlistentry>
@@ -256,192 +85,291 @@
       </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><userinput>case id (id1:t1) … (idn:tn)</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>
+	     <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> &TODO; </para>
+        <para>To be used in a proof by induction or by cases to start
+          a new case</para>
 	    </listitem>
 	 </varlistentry>
          <varlistentry>
             <term>Action:</term>
             <listitem>
-              <para> &TODO; </para>
+              <para>Starts the new case <command>id</command> declaring
+                the local parameters <command>(id1:t1) … (idn:tn)</command></para>
             </listitem>
          </varlistentry>
          <varlistentry>
            <term>New sequents to prove:</term>
            <listitem>
-               <para>&TODO;</para>
+               <para>None</para>
            </listitem>
          </varlistentry>
        </variablelist>
      </para>
   </sect1> 
 
+ <sect1 id="tac_bydone">
+   <title>done</title>
+   <titleabbrev>done</titleabbrev>
+   <para><userinput>justification done</userinput></para>
+   <para>
+     <variablelist>
+       <varlistentry role="tactic.synopsis">
+         <term>Synopsis:</term>
+	 <listitem>
+	   <para>&justification; <emphasis role="bold">done</emphasis></para>
+	 </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Pre-condition:</term>
+	 <listitem>
+	   <para></para>
+	 </listitem>
+       </varlistentry>
+       <varlistentry>
+         <term>Action:</term>
+	   <listitem> 
+	     <para>It closes the current sequent given the justification.</para>
+	   </listitem>
+       </varlistentry>
+       <varlistentry>
+           <term>New sequents to prove:</term>
+           <listitem>
+               <para>None.</para>
+           </listitem>
+       </varlistentry>
+   </variablelist>
+     </para>
+  </sect1>
+
+
+  <sect1 id="tac_exitselim">
+    <title>let such that</title>
+    <titleabbrev>let such that</titleabbrev>
+    <para><userinput>justification let x:t such that p (id)</userinput>
+    </para>
+    <para>
+      <variablelist>
+        <varlistentry role="tactic.synopsis">
+	  <term>Synopsis:</term>
+	  <listitem>
+	    <para>&justification; <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>
+	    </para>
+	  </listitem>  
+	</varlistentry>
+	<varlistentry>
+	  <term>Action:</term>
+	  <listitem>
+      <para>It derives <command>∃x:t.p</command> using the
+        <command>justification</command> and then it introduces in the context
+        <command>x</command> and the hypothesis  
+        <command>p</command> labelled with
+        <command>id</command>.
+      </para>
+	  </listitem>
+	</varlistentry>
+	<varlistentry>
+	  <term>New sequent to prove:</term>
+	  <listitem>
+      <para>None.</para>
+	  </listitem>
+	</varlistentry>
+     </variablelist>
+    </para>
+  </sect1>
+
   <sect1 id="tac_obtain">
-    <title>obtain/conclude</title>
-    <titleabbrev>obtain/conclude</titleabbrev>
-    <para><userinput>obtain H t=t [auto_params | exact t| proof | using t] done</userinput></para>
+    <title>obtain</title>
+    <titleabbrev>obtain</titleabbrev>
+    <para><userinput>obtain H t1 = t2 justification</userinput></para>
     <para>
       <variablelist>
          <varlistentry role="tactic.synopsis">
 	   <term>Synopsis:</term>
 	   <listitem>
-	     <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">exact</emphasis> &term; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
+	     <para>[<emphasis role="bold">obtain</emphasis> &id; | <emphasis role="bold">conclude</emphasis> &term;] <emphasis role="bold">=</emphasis> &term; [&autoparams; | <emphasis role="bold">using</emphasis> &term; | <emphasis role="bold">using once</emphasis> &term; | <emphasis role="bold">proof</emphasis>] [<emphasis role="bold">done</emphasis>]</para>
 	   </listitem>
 	 </varlistentry>
 	 <varlistentry>
 	   <term>Pre-condition:</term>
 	     <listitem>
-	       <para> &TODO; </para>
-	     </listitem>
+         <para><command>conclude</command> can be used only if the current
+           sequent is stating an equality. The left hand side must be omitted
+           in an equality chain.</para> 
+       </listitem>
 	 </varlistentry>
 	 <varlistentry>
 	   <term>Action:</term>
 	   <listitem>
-	      <para> &TODO; </para>
+       <para>Starts or continues an equality chain. If the chain starts 
+         with <command>obtain H</command> a new subproof named 
+         <command>H</command> is started.</para>
            </listitem>
          </varlistentry>
 	 <varlistentry>
-	   <term>New sequence to prove:</term>
+	   <term>New sequent to prove:</term>
 	     <listitem>
-	        <para> &TODO; </para>
+	        <para>If the chain starts 
+            with <command>obtain H</command> a nre sequent for
+            <command>t2 = ?</command> is opened.
+          </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>
+  <sect1 id="tac_suppose">
+    <title>suppose</title>
+    <titleabbrev>suppose</titleabbrev>
+    <para><userinput>suppose t1 (x) that is equivalent to t2</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> [ <emphasis role="bold">that is equivalent to</emphasis>  &term; ]</para>
+	 </listitem>
+       </varlistentry>
+      <varlistentry>
+         <term>Pre-condition:</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 proposition (i.e. <command>T</command> has type
+	   <command>Prop</command> or <command>CProp</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_thesisbecomes">
+     <title>the thesis becomes</title>
+     <titleabbrev>the 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">by</emphasis> &term; <emphasis role="bold">we proved</emphasis> &term; 
-	           <emphasis role="bold">(</emphasis> &id; <emphasis role="bold">)</emphasis></para>
-           </listitem>
+        <variablelist>
+	   <varlistentry role="tactic.synopsis">
+	     <term>Synopsis:</term>
+	     <listitem>
+	       <para><emphasis role ="bold">the thesis becomes</emphasis> &term; </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>
+         <para>The provided term <command>t</command> must be convertible with
+           current sequent.</para>
 	     </listitem>
 	   </varlistentry>
 	   <varlistentry>
 	     <term>Action:</term>
 	     <listitem>
-	       <para>It closes the current sequent by applying<command>th</command> to <command>t</command>.</para>
+	       <para>It changes the current goal to the one provided.</para>
 	     </listitem>
 	   </varlistentry>
 	   <varlistentry>
-	     <term>New sequence to prove:</term>
+	     <term>New sequent to prove:</term>
 	     <listitem>
-	       <para> &TODO; </para>
+	       <para>None.</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>
+   </sect1>
+   
+  <sect1 id="tac_weneedtoprove">
+    <title>we need to prove</title>
+    <titleabbrev>we need to prove</titleabbrev>
+    <para><userinput>we need to prove t1 (id) or equivalently t2</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>
+      <para><emphasis role="bold">we need to prove</emphasis> &term;
+        [<emphasis role="bold">(</emphasis>&id;
+        <emphasis role="bold">)</emphasis>]
+        [ <emphasis role="bold">or equivalently</emphasis> &term;]</para> 
 	  </listitem>
 	</varlistentry>
-	<varlistentry>
-	  <term>New sequence to prove:</term>
+        <varlistentry>
+          <term>Pre-condition:</term>
 	  <listitem>
-	    <para>It opens one new sequent. The names of the new hypotheses are picked by<command>t (id)</command> </para>
+	    <para></para>
 	  </listitem>
-	</varlistentry>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+	    <listitem>
+        <para>If <command>id</command> is provided, starts a subproof that once concluded 
+              will be named <command>id</command>. Otherwise states what needs to be proved.
+              If <command>t2</command> is provided, the new goal is 
+              immediately changed to <command>t2</command> wich must
+              be equivalent to <command>t1</command>.
+            </para>
+	    </listitem>
+        </varlistentry>
+        <varlistentry>
+           <term>New sequents to prove:</term>
+	   <listitem>
+	     <para>The stated one if <command>id</command> is provided</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>
+    <title>we have</title>
+    <titleabbrev>we have</titleabbrev>
+    <para><userinput>justification we have t1 (id1) and t2 (id2)</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; 
+	    <para>&justification; <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>
@@ -449,23 +377,142 @@
 	<varlistentry>
 	  <term>Pre-condition:</term>
 	  <listitem>
-	    <para><command>t</command> must be an logical type,type and  </para>
+	    <para></para>
 	  </listitem>
 	</varlistentry>
 	<varlistentry>
 	  <term>Action:</term>
 	  <listitem>
-	    <para>It proceeds on the values of <command>t</command>, according to the elimination principle </para>
+      <para>It derives <command>t1∧t2</command> using the 
+        <command>justification</command> then it introduces in the context
+        <command>t1</command>   labelled with <command>id1</command> and
+        <command>t2</command>   labelled with <command>id2</command>.
+      </para>
 	  </listitem>
 	</varlistentry>
 	<varlistentry>
-	  <term>New sequence to prove:</term>
+	  <term>New sequent 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>
+	     <para>None.</para>
           </listitem>
 	</varlistentry>
       </variablelist>
     </para>
   </sect1>
 
+  <sect1 id="tac_weproceedbycases">
+    <title>we proceed by cases on</title>
+      <titleabbrev>we proceed by cases on</titleabbrev>
+      <para><userinput>we proceed by cases on t to prove th</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><command>t</command> must inhabitant of an inductive type and
+          <command>th</command> must be the conclusion to be proved by 
+          cases.</para>
+	    </listitem>
+	  </varlistentry>
+	  <varlistentry>
+	    <term>Action:</term>
+	      <listitem>
+          <para> It proceeds by cases on <command>t</command> </para>
+              </listitem>
+	  </varlistentry>
+          <varlistentry>
+            <term>New sequents to prove:</term>
+	    <listitem>
+	       <para>It opens one new sequent for each constructor of the
+                type of <command>t</command>.</para>
+	    </listitem>
+	  </varlistentry>
+         </variablelist>
+       </para>
+    </sect1>
+    
+    <sect1 id="tac_weproceedbyinduction">
+    <title>we proceed by induction on</title>
+    <titleabbrev>we proceed by induction on</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 inhabitant of an inductive type and 
+        <command>th</command> must be the conclusion to be proved by induction.
+        </para>
+	  </listitem>
+	</varlistentry>
+	<varlistentry>
+	  <term>Action:</term>
+	    <listitem>
+	      <para>It proceed by induction on <command>t</command>.</para>
+	    </listitem>
+	</varlistentry>
+        <varlistentry>
+            <term>New sequents to prove:</term>
+            <listitem>
+              <para>It opens one new sequent for each constructor of the
+                type of <command>t</command>.</para>
+            </listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
+  </sect1>
+
+
+ <sect1 id="tac_bytermweproved">
+   <title>we proved</title>
+     <titleabbrev>we proved</titleabbrev>
+     <para><userinput>justification we proved t (id)</userinput></para>
+     <para>
+       <variablelist>
+         <varlistentry role="tactic.synopsis">
+	   <term>Synopsis:</term>
+	   <listitem>
+	     <para>&justification; <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>t</command>must have type <command>Prop</command>.
+         </para>
+	     </listitem>
+	   </varlistentry>
+	   <varlistentry>
+	     <term>Action:</term>
+	     <listitem>
+         <para>It derives <command>t</command>
+           using the justification and labels the conclusion with
+           <command>id</command>.
+         </para>
+	     </listitem>
+	   </varlistentry>
+	   <varlistentry>
+	     <term>New sequent to prove:</term>
+	     <listitem>
+	       <para>None.</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 6f247d04a..dbf1718f8 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -727,7 +727,6 @@
 
     <sect2 id="auto-params">
     <title>auto-params</title>
-    <para>&TODO;</para>
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>auto-params</title>
       <tgroup cols="4">
@@ -791,6 +790,29 @@
      </tgroup>
     </table>
     </sect2>
+
+    <sect2 id="justification">
+    <title>justification</title>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>justification</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="grammar.justification">&justification;</entry>
+  <entry>::=</entry>
+        <entry><emphasis role="bold">using</emphasis> &term;</entry>
+        <entry>Proof term manually provided</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>&autoparams;</entry>
+        <entry>Call automation</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    </sect2>
   </sect1>
 
 </chapter>
-- 
2.39.2