removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
authorwenzelm
Tue, 23 Nov 2021 21:43:45 +0100
changeset 74837 f0e0fc82b0b9
parent 74836 a97ec0954c50
child 74838 4c8d9479f916
removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
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 \<open>Some examples with text cartouches\<close>
 
 theory Cartouche_Examples
-imports Main
-keywords
-  "cartouche" :: diag and
-  "text_cartouche" :: thy_decl
+  imports Main
+  keywords "cartouche" :: diag
 begin
 
 subsection \<open>Regular outer syntax\<close>
@@ -135,14 +133,7 @@
 
 subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close>
 
-ML \<open>
-  Outer_Syntax.command
-    \<^command_keyword>\<open>text_cartouche\<close> ""
-    (Parse.opt_target -- Parse.input Parse.cartouche
-      >> Document_Output.document_output_markdown)
-\<close>
-
-text_cartouche
+text
 \<open>
   \<^ML>\<open>
       (