...

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index ac05db24a9bb9b3c122b74e046ac78639376321e..17adeb06f84a6d62513c69f6e3c978c0daac8190 100644 (file)
--- 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 6bedead7ffb0286f0abaa2fce4c6a3533be2f66a..8771aee6a9749e06141485f46f6e61693e5975da 100644 (file)
--- 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 63d436047f2dc3bbb86058991877fc56b072617d..289e400a92d43e0a8e854b5c462b963eceb6ce75 100644 (file)
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 9335dadf1f3339cffc1d3c231c1e22d70754b8ff..4a78164fbf95353e0f0b18e0b373194c87750c50 100644 (file)
--- 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 dcc7e9a81a86a15834228419c50ffdf9bf2b837b..3c0ba7090406c43aef3f0cbd8df79d2143efd902 100644 (file)
--- 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.