X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fmatita.xml;h=e20e17ad8db99f8527b184ff0a3254d0649519b0;hb=c31e50505b5afd8fb53236bd5d500c225471eb9a;hp=e32262ae44f7c7166b86390c541c42beca30661e;hpb=bdace32e5a6d981b418d076df176c5c79d856029;p=helm.git

diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml
index e32262ae4..e20e17ad8 100644
--- a/matita/help/C/matita.xml
+++ b/matita/help/C/matita.xml
@@ -8,13 +8,17 @@
   <!ENTITY gettingstarted SYSTEM "sec_gettingstarted.xml">
   <!ENTITY intro SYSTEM "sec_intro.xml">
   <!ENTITY terms SYSTEM "sec_terms.xml">
-  <!ENTITY tactics SYSTEM "sec_tactics.xml">
   <!ENTITY tacticals SYSTEM "sec_tacticals.xml">
+  <!ENTITY tactics SYSTEM "sec_tactics.xml">
+  <!ENTITY declarative_tactics SYSTEM "sec_declarative_tactics.xml">
   <!ENTITY othercommands SYSTEM "sec_commands.xml">
   <!ENTITY usernotation SYSTEM "sec_usernotation.xml">
 
+  <!ENTITY tacticref SYSTEM "tactics_quickref.xml">
+  <!ENTITY declarativetacticref SYSTEM "declarative_tactics_quickref.xml">
+
   <!ENTITY manrevision "1&alpha;">
-  <!ENTITY date "10/06/2006">
+  <!ENTITY date "12/07/2006">
   <!ENTITY app "<application>Matita</application>">
   <!ENTITY appname "Matita">
   <!ENTITY appversion SYSTEM "version.txt">
@@ -24,19 +28,29 @@
       url='http://www.mysql.com'>MySQL</ulink> </application>">
 
   <!-- Entities for BNF -->
-  <!ENTITY id "<emphasis><link linkend='id'>id</link></emphasis>">
-  <!ENTITY uri "<emphasis><link linkend='uri'>uri</link></emphasis>">
-  <!ENTITY char "<emphasis><link linkend='char'>char</link></emphasis>">
-  <!ENTITY uri-step "<emphasis><link linkend='uri-step'>uri-step</link></emphasis>">
-  <!ENTITY nat "<emphasis><link linkend='nat'>nat</link></emphasis>">
-  <!ENTITY term "<emphasis><link linkend='term'>term</link></emphasis>">
-  <!ENTITY match_pattern "<emphasis><link linkend='match_pattern'>match_pattern</link></emphasis>">
-  <!ENTITY args "<emphasis><link linkend='args'>args</link></emphasis>">
-  <!ENTITY args2 "<emphasis><link linkend='args2'>args2</link></emphasis>">
-  <!ENTITY sterm "<emphasis><link linkend='sterm'>sterm</link></emphasis>">
-  <!ENTITY intros-spec "<emphasis><link linkend='intros-spec'>intros-spec</link></emphasis>">
-  <!ENTITY pattern "<emphasis><link linkend='pattern'>pattern</link></emphasis>">
-  <!ENTITY reduction-kind "<emphasis><link linkend='reduction-kind'>reduction-kind</link></emphasis>">
+  <!ENTITY id "<emphasis><link linkend='grammar.id'>id</link></emphasis>">
+  <!ENTITY uri "<emphasis><link linkend='grammar.uri'>uri</link></emphasis>">
+  <!ENTITY char "<emphasis><link linkend='grammar.char'>char</link></emphasis>">
+  <!ENTITY uri-step "<emphasis><link linkend='grammar.uri-step'>uri-step</link></emphasis>">
+  <!ENTITY nat "<emphasis><link linkend='grammar.nat'>nat</link></emphasis>">
+  <!ENTITY term "<emphasis><link linkend='grammar.term'>term</link></emphasis>">
+  <!ENTITY rec_def "<emphasis><link linkend='grammar.rec_def'>rec_def</link></emphasis>">
+  <!ENTITY match_pattern "<emphasis><link linkend='grammar.match_pattern'>match_pattern</link></emphasis>">
+  <!ENTITY match_branch "<emphasis><link linkend='grammar.match_branch'>match_branch</link></emphasis>">
+  <!ENTITY args "<emphasis><link linkend='grammar.args'>args</link></emphasis>">
+  <!ENTITY args2 "<emphasis><link linkend='grammar.args2'>args2</link></emphasis>">
+  <!ENTITY sterm "<emphasis><link linkend='grammar.sterm'>sterm</link></emphasis>">
+  <!ENTITY intros-spec "<emphasis><link linkend='grammar.intros-spec'>intros-spec</link></emphasis>">
+  <!ENTITY pattern "<emphasis><link linkend='grammar.pattern'>pattern</link></emphasis>">
+  <!ENTITY reduction-kind "<emphasis><link linkend='grammar.reduction-kind'>reduction-kind</link></emphasis>">
+  <!ENTITY path "<emphasis><link linkend='grammar.path'>path</link></emphasis>">
+  <!ENTITY proofscript "<emphasis><link linkend='grammar.proofscript'>proof-script</link></emphasis>">
+  <!ENTITY proofstep "<emphasis><link linkend='grammar.proofstep'>proof-step</link></emphasis>">
+  <!ENTITY tactic "<emphasis><link linkend='grammar.tactic'>tactic</link></emphasis>">
+  <!ENTITY LCFtactical "<emphasis><link linkend='grammar.LCFtactical'>LCF-tactical</link></emphasis>">
+  <!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>">
 ]>
 
 <?yelp:chunk-depth 3?>
@@ -67,6 +81,13 @@
 	  <address> <email>sacerdot@cs.unibo.it</email> </address> 
 	</affiliation> 
       </author> 
+      <author> 
+	<firstname>Ferruccio</firstname> 
+	<surname>Guidi</surname> 
+	<affiliation> 
+	  <address> <email>fguidi@cs.unibo.it</email> </address> 
+	</affiliation> 
+      </author>       
       <author> 
 	<firstname>Enrico</firstname> 
 	<surname>Tassi</surname> 
@@ -81,13 +102,6 @@
 	  <address> <email>zacchiro@cs.unibo.it</email> </address> 
 	</affiliation> 
       </author>
-      <author> 
-	<firstname>Ferruccio</firstname> 
-	<surname>Guidi</surname> 
-	<affiliation> 
-	  <address> <email>fguidi@cs.unibo.it</email> </address> 
-	</affiliation> 
-      </author>       
     </authorgroup>
 
     <legalnotice>
@@ -113,8 +127,9 @@
 &gettingstarted;
 &terms;
 &usernotation;
-&tactics;
 &tacticals;
+&tactics;
+&declarative_tactics;
 &othercommands;
 &license;