From: Enrico Tassi 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;ds=sidebyside;h=3950e9607ece9ab2f46e1e48f3b7366b775deefb;hp=d589a4d7b25687c14510efb641f7e5eacc41fd6d;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; }