...

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 9eab214d6b493e5f0058f72263bef9a20ba63417..f15bdfd4edd3681322f137a1657a9de75d3ed60d 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -107,7 +107,7 @@ computation).
 
 Since we are going to formalize constructive and predicative mathematics
 in an intensional type theory like CIC, we try to establish some terminology. 
-Type is the sort of sets equipped with the `Id `equality (i.e. an intensional,
+Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
 not quotiented set). We will avoid using `Id` (Leibnitz equality), 
 thus we will explicitly equip a set with an equivalence relation when needed.
 We will call this structure a _setoid_. Note that we will

diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml
index 66f62acbe54d826dd86e9d7caf3492069f49d8a2..65351001c04d58c937f1a8a933ed919d287f7623 100644 (file)
--- a/helm/software/matita/nlibrary/topology/preamble.xml
+++ b/helm/software/matita/nlibrary/topology/preamble.xml
@@ -7,11 +7,14 @@ pre, code {
        font-family: monospace; 
 }
 
-p code {
+p code, li code {
        font-size: 130%;
        border-style: dashed;
        border-width: 1px;
-       padding: 0.2em;
+       padding-top: 0.2em;
+       padding-bottom: 0.2em;
+       padding-left: 0.3em;
+       padding-right: 0.3em;
        line-height: 1.8em;
        border-color: grey;
 }