fixes backported from the new kernel

[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..8aba5a08c16c4a073a9c0bfdb6817e3c6b94049c 100644 (file)
--- a/helm/software/matita/help/C/declarative_tactics_quickref.xml
+++ b/helm/software/matita/help/C/declarative_tactics_quickref.xml
@@ -48,7 +48,7 @@
       <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>[<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>
       </row>
       <row>
         <entry/>