# HG changeset patch # User wenzelm # Date 1637700225 -3600 # Node ID f0e0fc82b0b94c5c4671e5f6d582d5507ee7c00a # Parent a97ec0954c50b795659a02f45c410e1742095618 removed pointless 'text_cartouche' command: regular 'text' already supports cartouches; diff -r a97ec0954c50 -r f0e0fc82b0b9 src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Tue Nov 23 21:02:13 2021 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Tue Nov 23 21:43:45 2021 +0100 @@ -5,10 +5,8 @@ section \Some examples with text cartouches\ theory Cartouche_Examples -imports Main -keywords - "cartouche" :: diag and - "text_cartouche" :: thy_decl + imports Main + keywords "cartouche" :: diag begin subsection \Regular outer syntax\ @@ -135,14 +133,7 @@ subsubsection \Uniform nesting of sub-languages: document source, ML, term, string literals\ -ML \ - Outer_Syntax.command - \<^command_keyword>\text_cartouche\ "" - (Parse.opt_target -- Parse.input Parse.cartouche - >> Document_Output.document_output_markdown) -\ - -text_cartouche +text \ \<^ML>\ (