src/HOL/Data_Structures/Braun_Tree.thy
changeset 76987 4c275405faae
parent 72566 831f17da1aab
--- 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" |