From 3950e9607ece9ab2f46e1e48f3b7366b775deefb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 16:59:55 +0000 Subject: [PATCH 1/1] ... --- helm/software/matita/nlibrary/topology/igft.ma | 2 +- helm/software/matita/nlibrary/topology/preamble.xml | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) 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; } -- 2.39.2