src/HOL/Library/Tree.thy

--- a/src/HOL/Library/Tree.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Tree.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -8,8 +8,8 @@
 begin
 
 datatype 'a tree =
-  Leaf ("\<langle>\<rangle>") |
-  Node "'a tree" ("value": 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
+  Leaf (\<open>\<langle>\<rangle>\<close>) |
+  Node "'a tree" ("value": 'a) "'a tree" (\<open>(1\<langle>_,/ _,/ _\<rangle>)\<close>)
 datatype_compat tree
 
 primrec left :: "'a tree \<Rightarrow> 'a tree" where