...

[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 1cb932184a64e9fc03d69969a52865a18e0018c1..a4ac5d46914340de617c304a9b3d40937c53113a 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -16,14 +16,16 @@ The tutorial spends a considerable amount of effort in defining
 notations that resemble the ones used in the original paper. We believe
 this a important part of every formalization, not only for the estetic 
 point of view, but also from the practical point of view. Being 
-consistent allows to follow the paper in a pedantic way. 
+consistent allows to follow the paper in a pedantic way, and hopefully
+to make the formalization (at least the definitions and proved
+statements) readable to the author of the paper. 
 
 Orientering
 -----------
 
 TODO 
 
-buttons, PG-interaction-model, sequent window, script window
+buttons, PG-interaction-model, sequent window, script window, ncheck
 
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):