]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Oct 2009 16:59:55 +0000 (16:59 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Oct 2009 16:59:55 +0000 (16:59 +0000)
helm/software/matita/nlibrary/topology/igft.ma
helm/software/matita/nlibrary/topology/preamble.xml

index 9eab214d6b493e5f0058f72263bef9a20ba63417..f15bdfd4edd3681322f137a1657a9de75d3ed60d 100644 (file)
@@ -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. 
 
 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 `Idequality (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
 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
index 66f62acbe54d826dd86e9d7caf3492069f49d8a2..65351001c04d58c937f1a8a933ed919d287f7623 100644 (file)
@@ -7,11 +7,14 @@ pre, code {
        font-family: monospace; 
 }
 
        font-family: monospace; 
 }
 
-p code {
+p code, li code {
        font-size: 130%;
        border-style: dashed;
        border-width: 1px;
        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;
 } 
        line-height: 1.8em;
        border-color: grey;
 }