X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fdeclarative_tactics_quickref.xml;fp=matita%2Fhelp%2FC%2Fdeclarative_tactics_quickref.xml;h=8aba5a08c16c4a073a9c0bfdb6817e3c6b94049c;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/help/C/declarative_tactics_quickref.xml b/matita/help/C/declarative_tactics_quickref.xml
new file mode 100644
index 000000000..8aba5a08c
--- /dev/null
+++ b/matita/help/C/declarative_tactics_quickref.xml
@@ -0,0 +1,71 @@
+<table frame="topbot" rowsep="0" colsep="0" role="grammar">
+  <title>tactics</title>
+  <tgroup cols="3">
+    <tbody>
+      <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>
+      </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>
+      </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>
+      </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>
+      </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>
+      </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>
+      </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>
+      </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>
+      </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>
+      </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>
+      </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">the thesis becomes</emphasis> <emphasis><link linkend="grammar.sterm">sterm</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>
+      </row>
+    </tbody>
+  </tgroup>
+</table>