From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 18 Oct 2009 18:46:36 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3279
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=89e21dbecca75a5320f50ecb53a39699f8ace8f1;hp=7fd4f2f66fb8fe010bbd2bfe1f6b542c2da6c83f;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index ac05db24a..17adeb06f 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,12 +1,12 @@
 logic/cprop.ma hints_declaration.ma sets/setoids1.ma
 sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
-topology/igft.ma sets/sets.ma
+topology/igft.ma logic/equality.ma sets/sets.ma
 datatypes/bool.ma logic/pts.ma
 sets/setoids1.ma properties/relations1.ma sets/setoids.ma
 logic/equality.ma logic/connectives.ma properties/relations.ma
 sets/setoids.ma logic/connectives.ma properties/relations.ma
 logic/connectives.ma logic/pts.ma
-topology/cantor.ma topology/igft.ma
+topology/cantor.ma nat/nat.ma topology/igft.ma
 datatypes/pairs.ma logic/pts.ma
 algebra/abelian_magmas.ma algebra/magmas.ma
 nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 6bedead7f..8771aee6a 100644
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -9,6 +9,7 @@ digraph g {
   "sets/sets.ma" -> "properties/relations1.ma" [];
   "sets/sets.ma" -> "sets/setoids1.ma" [];
   "topology/igft.ma" [];
+  "topology/igft.ma" -> "logic/equality.ma" [];
   "topology/igft.ma" -> "sets/sets.ma" [];
   "datatypes/bool.ma" [];
   "datatypes/bool.ma" -> "logic/pts.ma" [];
@@ -24,6 +25,7 @@ digraph g {
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.ma" [];
   "topology/cantor.ma" [];
+  "topology/cantor.ma" -> "nat/nat.ma" [];
   "topology/cantor.ma" -> "topology/igft.ma" [];
   "datatypes/pairs.ma" [];
   "datatypes/pairs.ma" -> "logic/pts.ma" [];
diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index 63d436047..289e400a9 100644
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ
diff --git a/helm/software/matita/nlibrary/topology/Makefile b/helm/software/matita/nlibrary/topology/Makefile
index 9335dadf1..4a78164fb 100644
--- a/helm/software/matita/nlibrary/topology/Makefile
+++ b/helm/software/matita/nlibrary/topology/Makefile
@@ -6,7 +6,8 @@ print: $(SRC:%.ma=%.pdf)
 
 %.pdf: %.html
 	# requires http://torisugari.googlepages.com/commandlineprint2
-	iceweasel -print $< -printmode pdf -printfile ./$@
+	touch $@
+	iceweasel -print file://$$PWD/$< -printmode PDF -printfile ./$@
 
 clean:
 	rm *.html *.png *.mdwn
diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index dcc7e9a81..3c0ba7090 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -240,7 +240,7 @@ reaching the end of the formalization, but we had to assume the proof
 of the extensionality of the `U_x` construction (while there is no
 need to assume the same property for `F_x`!). 
 
-The current version of the formaliztion uses `Id`. 
+The current version of the formalization uses `Id`. 
 
 The standard library and the `include` command
 ----------------------------------------------
@@ -923,11 +923,11 @@ Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
 
 That, up to rewriting with the equation defining `x`, is what we mean.
 Since we decided to use `Id` the rewriting always work (the elimination
-prnciple for `Id` is Leibnitz's equality, that is quantified over
+principle for `Id` is Leibnitz's equality, that is quantified over
 the context. 
 
 The problem that arises if we decide to make `S` a setoid is that 
-`V` has to be extensional w.r.t. the equality of `S` (i.e. the charactestic
+`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic
 functional proposition has to quotient its input with a relation bigger
 than the one of `S`.
 
@@ -1013,7 +1013,7 @@ there is still some work to do.
 D[retr-3]
 To use the equation defining `b` we have to eliminate `H`. Unfolding
 definitions in `x` tell us there is still something to do. The `nrewrite`
-tactic is a shorcut for the elimination principle of the equlity.
+tactic is a shortcut for the elimination principle of the equality.
 It accepts an additional argument `<` or `>` to rewrite left-to-right
 or right-to-left.