X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=3deaf4b517ae381d6f1bfe0419f22de521c83278;hb=8f699ab265e380a2d1ab7dba0ee5e8ba5556a84a;hp=7e22f33043d39ec5e0fcb62e7ce0c20ca1e41593;hpb=ddc80515997a3f56085c6234d4db326141e189aa;p=helm.git
diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml
index 7e22f3304..3deaf4b51 100644
--- a/matita/matita/help/C/sec_commands.xml
+++ b/matita/matita/help/C/sec_commands.xml
@@ -60,7 +60,7 @@
Synopsis:
- check &term;
+ check &sterm;
@@ -74,6 +74,7 @@
+
+
coercion
+ TODO
+
+
+
include
include "s"
@@ -323,6 +334,7 @@
+
+
qed
qed
@@ -401,7 +416,33 @@
+
+ qed-
+ qed-
+
+
+
+ Synopsis:
+
+ qed-
+
+
+
+
+ Action:
+
+ Saves the current interactive theorem or
+ definition without indexing. Therefore automation will ignore
+ it.
+ In order to do this, the set of sequents still to be proved
+ must be empty.
+
+
+
+
+
+