--- a/src/HOL/ex/Code_Lazy_Demo.thy Thu Oct 24 22:05:57 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Fri Oct 25 11:31:16 2024 +0200
@@ -113,7 +113,8 @@
= L (\<open>\<spadesuit>\<close>)
| Node tree tree (infix \<open>\<triangle>\<close> 900)
-notation (output) Node (\<open>\<triangle>(//\<^bold>l: _//\<^bold>r: _)\<close>)
+notation (output) Node
+ (\<open>(\<open>indent=1 notation=\<open>mixfix tree node\<close>\<close>\<triangle>//(\<open>open_block notation=\<open>mixfix tree branch\<close>\<close>\<^bold>l: _)//(\<open>open_block notation=\<open>mixfix tree branch\<close>\<close>\<^bold>r: _))\<close>)
code_lazy_type tree