]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/help/C/tactics_quickref.xml
decompose: delta-expansion of the type to eliminate now works fine
[helm.git] / matita / help / C / tactics_quickref.xml
index 47e237e86c08b960bdaf2a183f3e59423c0ca82a..70d42ac2b59891d92a7614952cde0d91706a6856 100644 (file)
         <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>