From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Oct 2009 16:59:55 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3311
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3950e9607ece9ab2f46e1e48f3b7366b775deefb;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 9eab214d6..f15bdfd4e 100644
--- 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 66f62acbe..65351001c 100644
--- 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;
 }