rendering fixes

IsarMathLib/MetricSpace_ZF_1.thy

@@ -44,8 +44,8 @@ text\<open> The \<open>reals\<close> context (locale) defined in the \<open>Real
   positive numbers, absolute value etc. For metric spaces we reuse the notation defined there.\<close>
 
 text\<open>The \<open>pmetric_space1\<close> locale extends the \<open>reals\<close> locale, adding the carrier $X$ 
-  of the metric space and the metric $\mathfrak{d}$ to the context, together with the assumption
-  that $\mathfrak{d}:X\times X \rightarrow \mathbb{R}$ is a pseudo metric.
+  of the metric space and the metric $\mathcal{d}$ to the context, together with the assumption
+  that $\mathcal{d}:X\times X \rightarrow \mathbb{R}^+$ is a pseudo metric.
   An alternative would be to define the \<open>pmetric_space1\<close> as an extension of the \<open>pmetric_space1\<close>
   context, but that is in turn an extension of the \<open>loop1\<close> locale that defines notation
   for left and right division which which do not want in the context of real numbers. \<close>

IsarMathLib/Topology_ZF_examples.thy

@@ -224,19 +224,17 @@ proof-
   ultimately show ?thesis by auto
 qed
 
-text\<open> $X$ is a closed set that contains $A$.
-This lemma is necessary because we cannot
-use the lemmas proven in the \<open>topology0\<close> context since
-\<open> T\<noteq>0"} \<close> is too weak for
- \<open>CoCardinal(X,T)\<close> to be a topology.\<close>
+text\<open> $X$ is a closed set that contains $A$. 
+  This lemma is necessary because we cannot use the lemmas proven in the 
+  \<open>topology0\<close> context since $T\<noteq>0$ is too weak for \<open>CoCardinal(X,T)\<close> 
+  to be a topology.\<close>
 
 lemma X_closedcov_cocardinal:
   assumes "T\<noteq>0" "A\<subseteq>X"
-  shows "X\<in>ClosedCovers(A,CoCardinal(X,T))" using ClosedCovers_def
+  shows "X \<in> ClosedCovers(A,CoCardinal(X,T))" using ClosedCovers_def
   using union_cocardinal closed_sets_cocardinal assms by auto
 
-text\<open>The closure of a set is itself if it is closed or \<open>X\<close> if
-it isn't closed.\<close>
+text\<open>The closure of a set is itself if it is closed or $X$ if it isn't closed.\<close>
 
 lemma closure_set_cocardinal:
   assumes "T\<noteq>0""A\<subseteq>X"

isar2html2.0/src/isar2html/IsarSym2Latex.fs

@@ -123,6 +123,7 @@ namespace iml
                  ("\\<S>", "\\mathcal{S} ")
                  ("\\<T>", "\\mathcal{T} ")
                  ("\\<X>", "\\mathcal{X} ")
+                 ("\\<d>", "\\mathcal{d} ")
                  ("\\<ra>", " + ")
                  ("\\<rd>", "/ ")
                  ("\\<rm>", " - ")