changeset 80768 | c7723cc15de8 |
parent 69597 | ff784d5a5bfb |
child 80786 | 70076ba563d2 |
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 20:54:20 2024 +0200 +++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Sun Aug 25 21:10:01 2024 +0200 @@ -24,6 +24,7 @@ no_notation lazy_llist ("_") syntax "_llist" :: "args => 'a list" ("\<^bold>[(_)\<^bold>]") +syntax_consts "_llist" == lazy_llist translations "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"