X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=dbb6900d98f9d92d17184070315b0e7adf6d42f9;hb=ca7327c20c6031829fade8bb84a3a1bb66113f54;hp=9a968e5c970baccfceeb48f07ee7f85c1498926f;hpb=68aad189a157255485177a8a632d44ac3ad73a09;p=helm.git

diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml
index 9a968e5c9..dbb6900d9 100644
--- a/matita/matita/help/C/sec_terms.xml
+++ b/matita/matita/help/C/sec_terms.xml
@@ -453,6 +453,41 @@
      <command>f</command> must be defined by means of tactics.</para>
     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
   </sect2>
+  <sect2 id="discriminator">
+    <title><emphasis role="bold">discriminator</emphasis> &id;</title>
+    <titleabbrev>discriminator</titleabbrev>
+    <para><userinput>discriminator i</userinput></para>
+    <para>Defines a new discrimination (injectivity+conflict) principle à la 
+     McBride for the inductive type <command>i</command>.</para> 
+    <para>The principle will use John 
+     Major's equality if such equality is defined, otherwise it will use 
+     Leibniz equality; in the former case, it will be called 
+     <command>i_jmdiscr</command>, in the latter, <command>i_discr</command>. 
+     The command will fail if neither equality is available.</para>   
+    <para>Discrimination principles are used by the destruct tactic and are 
+     usually automatically generated by Matita during the definition of the 
+     corresponding inductive type. This command is thus especially useful 
+     when the correct equality was not loaded at the time of that 
+     definition.</para>
+  </sect2>
+  <sect2 id="inverter">
+    <title><emphasis role="bold">inverter</emphasis> &id; <emphasis role="bold">for</emphasis> &id; (&path;) [&term;]</title>
+    <titleabbrev>inverter</titleabbrev>
+    <para><userinput>inverter n for i (path) : s</userinput></para>
+    <para>Defines a new induction/inversion principle for the inductive type
+     <command>i</command>, called <command>n</command>.</para>
+    <para><command>(path)</command> must be in the form <command>(# # # ... #)</command>, 
+     where each <command>#</command> can be either <command>?</command> or 
+     <command>%</command>, and the number of symbols is equal to the number of 
+     right parameters (indices) of <command>i</command>. Parentheses are 
+     mandatory. If the j-th symbol is 
+     <command>%</command>, Matita will generate a principle providing 
+     equations for reasoning on the j-th index of <command>i</command>. If the
+     symbol is a <command>?</command>, no corresponding equation will be 
+     provided.</para>
+    <para><command>s</command>, which must be a sort, is the target sort of the
+     induction/inversion principle and defaults to <command>Prop</command>.</para>
+  </sect2>
   <sect2 id="letrec">
     <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
     <titleabbrev>&TODO;</titleabbrev>
@@ -601,18 +636,18 @@
        <row>
 	<entry id="grammar.pattern">&pattern;</entry>
 	<entry>::=</entry>
-        <entry><emphasis role="bold">{</emphasis>
+        <entry><emphasis role="bold">in</emphasis>
           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
-          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
         <entry>simple pattern</entry>
        </row>
        <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">{match</emphasis> &path;
+        <entry><emphasis role="bold">in</emphasis> <emphasis role="bold">match</emphasis> &path;
           [<emphasis role="bold">in</emphasis>
           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
-          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
         <entry>full pattern</entry>
        </row>
       </tbody>
@@ -620,7 +655,7 @@
     </table>
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>path</title>
-      <tgroup cols="4">
+      <tgroup cols="3">
       <tbody>
        <row>
 	<entry id="grammar.path">&path;</entry>