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

diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml
index 89d9ee658..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">
@@ -39,6 +43,14 @@
   <!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?>
@@ -69,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> 
@@ -83,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>
@@ -115,8 +127,9 @@
 &gettingstarted;
 &terms;
 &usernotation;
-&tactics;
 &tacticals;
+&tactics;
+&declarative_tactics;
 &othercommands;
 &license;