cantor...

[helm.git] / helm / software / matita / nlibrary / topology / igft.ma

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 06f2c08e5d18f019b6c5fe9fde0c7ebec68f4ada..21194951bc91831f211012245fae1737f245f311 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -25,8 +25,13 @@ statements) readable to the author of the paper.
 The formalization uses the ng (new generation) version of Matita
 (that will be named 1.x when finally released). 
 Last stable release of the "old" system is named 0.5.7; the ng system
-is coexisting with the old one in every development release with a 
-version strictly greater than 0.5.7.
+is coexisting with the old one in every development release 
+(named "nightly builds" in the download page of Matita) 
+with a version strictly greater than 0.5.7.
+
+To read this tutorial in HTML format, you need a decent browser
+equipped with a unicode capable font. Use the PDF format if some
+symbols are not displayed correctly.
 
 Orienteering
 ------------
@@ -977,6 +982,8 @@ We now proceed with the proof of the infinity rule.
 D*)
 
 
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
 alias symbol "covers" = "new covers set".
 ntheorem new_coverage_infinity:
   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.