more on screenshot

[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 87aca5dcfacfb0a299c7a9debff86ca36aa18735..50a62bff4ec049e749c5429ef2b16707bb44ddfd 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -11,7 +11,7 @@ Initial setup
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):
 
-- `Ω` \Omega 
+- `Ω` can be typed \Omega 
 - `∀` \Forall
 - `λ` \lambda
 - `≝` \def
@@ -63,6 +63,8 @@ interpretation "C" 'C a i = (C ? a i).
 The first definition
 --------------------
 
+![bla bla][def-fish-rec]
+
 DOCEND*)
 
 ndefinition cover_set ≝ λc:∀A:Ax.Ω^A → A → CProp[0].λA,C,U.
@@ -105,7 +107,7 @@ nlet corec fish_rec (A:Ax) (U: Ω^A)
  (P: Ω^A) (H1: P ⊆ U)
   (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P):
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
-#a; #p; napply cfish; (** screenshot "topology/def-fish-rec". *)
+#a; #p; napply cfish; (** screenshot "def-fish-rec". *)
 ##[ napply H1; napply p;
 ##| #i; ncases (H2 a p i); #x; *; #xC; #xP; @; ##[napply x]
     @; ##[ napply xC ] napply (fish_rec ? U P); nassumption;