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. - - - - - whelp whelp locate "s"