| changeset 76987 | 4c275405faae |
| parent 71255 | 4258ee13f5d4 |
| child 78277 | 6726b20289b4 |
--- a/src/HOL/Analysis/Continuous_Extension.thy Sun Jan 15 16:28:03 2023 +0100 +++ b/src/HOL/Analysis/Continuous_Extension.thy Sun Jan 15 18:30:18 2023 +0100 @@ -296,7 +296,7 @@ subsection\<open>Dugundji's Extension Theorem and Tietze Variants\<close> -text \<open>See \cite{dugundji}.\<close> +text \<open>See \<^cite>\<open>"dugundji"\<close>.\<close> lemma convex_supp_sum: assumes "convex S" and 1: "supp_sum u I = 1"