# HG changeset patch
# User wenzelm
# Date 1729848676 -7200
# Node ID be68bb67140d0e828050791ad894a877119a617d
# Parent  bbed9f218158672aec885455a84d65b718cbeb2c
more inner-syntax markup;

diff -r bbed9f218158 -r be68bb67140d src/HOL/ex/Code_Lazy_Demo.thy
--- 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