...

[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 
 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 
 
 
 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):
 
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):