...

[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 96f419aa33ebf03269bd40264dd2edd825b866bc..d0068dbf7e5f367c05f1b72616f132091b78834a 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,17 @@ 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 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
 ------------
 
@@ -72,6 +84,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
@@ -366,7 +383,7 @@ of the inductive predicate) on the right of `:`.
 
 D*)
 
-(* ncheck xcreflexivity. *)
+(** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
 
 (*D
 
@@ -544,7 +561,7 @@ but not introduction rules for the coinductive case.
 
 D*)
 
-(* ncheck cover_rect_CProp0. *) 
+(** ncheck cover_rect_CProp0. *) 
 
 (*D