...

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index e98696589e2f30f48fdfa9011a8df7c1c2692285..2d769264816dc98baab61625b463a9334cadab09 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -11,6 +11,7 @@ the formalization of the paper
 > inductive generation of formal topologies
 
 by Stefano Berardi and Silvio Valentini. 
+
 The tutorial is by Enrico Tassi. 
 
 The tutorial spends a considerable amount of effort in defining 
@@ -21,6 +22,12 @@ 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. 
 
+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 cohexisting with the old one in every development release with a 
+version strictly grater then 0.5.7.
+
 Orienteering
 ------------
 
@@ -72,6 +79,11 @@ implements two unusual input facilities:
   example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, … 
   Variants are listed in the aforementioned TeX/UTF-8 table. 
 
+The syntax of terms (and types) is the one of the λ-calculus CIC
+on which Matita is based. The main syntactical difference w.r.t. 
+the usual mathematical notation is the function application, written
+`(f x y)` in place of `f(x,y)`. 
+
 Pressing `F1` opens the Matita manual.
 
 CIC (as [implemented in Matita][3]) in a nutshell