X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_commands.xml;h=5e55de9994648e7768358c6751f7eb2b96dbb589;hb=ddb5e7c8313d80b2bc1b452f14d531d143d102c6;hp=636eac8dc236a66cb744ca5fa8d59e2c5c86ed50;hpb=65317d14f32bc24b3e9ed4ea144833dd8517773a;p=helm.git
diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml
index 636eac8dc..5e55de999 100644
--- a/helm/software/matita/help/C/sec_commands.xml
+++ b/helm/software/matita/help/C/sec_commands.xml
@@ -139,7 +139,7 @@
clusters
-
+
name
@@ -148,6 +148,12 @@
expected object for 3rd URI
expected object for 4th URI
expected 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