--- a/src/HOL/Data_Structures/Braun_Tree.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Data_Structures/Braun_Tree.thy Sun Jan 15 18:30:18 2023 +0100
@@ -6,8 +6,8 @@
imports "HOL-Library.Tree_Real"
begin
-text \<open>Braun Trees were studied by Braun and Rem~\cite{BraunRem}
-and later Hoogerwoord~\cite{Hoogerwoord}.\<close>
+text \<open>Braun Trees were studied by Braun and Rem~\<^cite>\<open>"BraunRem"\<close>
+and later Hoogerwoord~\<^cite>\<open>"Hoogerwoord"\<close>.\<close>
fun braun :: "'a tree \<Rightarrow> bool" where
"braun Leaf = True" |