author | wenzelm |
Tue, 09 Jan 2018 00:16:23 +0100 | |
changeset 67382 | 39e4668ded4f |
parent 67381 | 146757999c8d |
child 67383 | aacea75450b4 |
--- a/src/HOL/ex/Cartouche_Examples.thy Mon Jan 08 23:45:43 2018 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Tue Jan 09 00:16:23 2018 +0100 @@ -141,7 +141,7 @@ Outer_Syntax.command @{command_keyword text_cartouche} "" (Parse.opt_target -- Parse.input Parse.cartouche - >> Thy_Output.document_command {markdown = true}) + >> Pure_Syn.document_command {markdown = true}) \<close> text_cartouche