X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=4fe77d7b78a8dc3e4871322b5d6a5c736ce11ccb;hb=6beaf573e5639ddba6b55488e44aa6d4f298b052;hp=1644c85bd88493728d926261f9b32211cb123a2c;hpb=c766ed6f754196fe55254d09189f1255054b95f1;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 1644c85bd..4fe77d7b7 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -148,6 +148,12 @@
expected object for 3rd URIexpected object for 4th URIexpected object for 5th URI
+ expected object for 6th URI
+ expected object for 7th URI
+ expected object for 8th URI
+ expected object for 9th URI
+ expected object for 10th URI
+ expected object for 11th URI
@@ -158,6 +164,12 @@
a theorem of type âA.âx,y,z:A.eq A x y â eq A y z â eq A x zâA.âa.â P:A âProp.P x âây.eq A x y â P yâA.âa.â P:A âProp.P x âây.eq A y x â P y
+ âA.âa.â P:A âSet.P x âây.eq A x y â P y
+ âA.âa.â P:A âSet.P x âây.eq A y x â P y
+ âA.âa.â P:A âType.P x âây.eq A x y â P y
+ âA.âa.â P:A âType.P x âây.eq A y x â P y
+ âA.âB.â f:A â B.âx,y:A.eq A x y â eq B (f x) (f y)
+ âA.âB.â f:A â B.âx,y:A.eq A x y â eq B (f y) (f x)true
@@ -242,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.
@@ -270,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"