X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=4fe77d7b78a8dc3e4871322b5d6a5c736ce11ccb;hb=04d8e2282a3536a9b822a8dbfcbdb4e3a949f04d;hp=5e55de9994648e7768358c6751f7eb2b96dbb589;hpb=b3488620204bbc7ea656c45096a703ff15160bd5;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 5e55de999..4fe77d7b7 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -254,8 +254,7 @@
On the contrary, theorem and definitions declared in a file can be
immediately used without including it.
The file s is automatically compiled
- if it is not compiled yet and if it is handled by a
- development.
+ if it is not compiled yet.
@@ -282,36 +281,6 @@
-
- set
- set "baseuri" "s"
-
-
-
- Synopsis:
-
- set &qstring; &qstring;
-
-
-
- Action:
-
- Sets to s the baseuri of all the
- theorems and definitions stated in the current file.
- The baseuri should be a/b/c/foo
- if the file is named foo and it is in
- the subtree a/b/c of the current
- development.
- This requirement is not enforced, but it could be in the future.
-
- Currently, baseuri is the only
- property that can be set even if the parser accepts
- arbitrary property names.
-
-
-
-
- whelpwhelp locate "s"