author | wenzelm |
Tue, 23 Nov 2021 17:14:55 +0100 | |
changeset 74834 | 8d7d082c1649 |
parent 74833 | fe9e590ae52f |
child 74835 | 26c3a9c92e11 |
--- a/src/HOL/ex/Cartouche_Examples.thy Tue Nov 23 16:06:09 2021 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Tue Nov 23 17:14:55 2021 +0100 @@ -139,7 +139,7 @@ Outer_Syntax.command \<^command_keyword>\<open>text_cartouche\<close> "" (Parse.opt_target -- Parse.input Parse.cartouche - >> Pure_Syn.document_command {markdown = true}) + >> Document_Output.document_output_markdown) \<close> text_cartouche