doc-src/IsarRef/Thy/Document_Preparation.thy

     @{antiquotation_def "term"} & : & @{text antiquotation} \\
     @{antiquotation_def const} & : & @{text antiquotation} \\
     @{antiquotation_def abbrev} & : & @{text antiquotation} \\
     @{antiquotation_def typeof} & : & @{text antiquotation} \\
     @{antiquotation_def typ} & : & @{text antiquotation} \\
-    @{antiquotation_def thm_style} & : & @{text antiquotation} \\
-    @{antiquotation_def term_style} & : & @{text antiquotation} \\
     @{antiquotation_def "text"} & : & @{text antiquotation} \\
     @{antiquotation_def goals} & : & @{text antiquotation} \\
     @{antiquotation_def subgoals} & : & @{text antiquotation} \\
     @{antiquotation_def prf} & : & @{text antiquotation} \\
     @{antiquotation_def full_prf} & : & @{text antiquotation} \\

     atsign lbrace antiquotation rbrace
     ;
 
     antiquotation:
       'theory' options name |
-      'thm' options thmrefs |
+      'thm' options styles thmrefs |
       'lemma' options prop 'by' method |
-      'prop' options prop |
-      'term' options term |
+      'prop' options styles prop |
+      'term' options styles term |
       'const' options term |
       'abbrev' options term |
       'typeof' options term |
       'typ' options type |
-      'thm\_style' options name thmref |
-      'term\_style' options name term |
       'text' options name |
       'goals' options |
       'subgoals' options |
       'prf' options thmrefs |
       'full\_prf' options thmrefs |

     ;
     options: '[' (option * ',') ']'
     ;
     option: name | name '=' name
     ;
+    styles: '(' (style * ',') ')'
+    ;
+    style: (name *)
+    ;
   \end{rail}
 
   Note that the syntax of antiquotations may \emph{not} include source
   comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
   text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim

   \item @{text "@{typeof t}"} prints the type of a well-typed term
   @{text "t"}.
 
   \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
   
-  \item @{text "@{thm_style s a}"} prints theorem @{text a},
-  previously applying a style @{text s} to it (see below).
-  
-  \item @{text "@{term_style s t}"} prints a well-typed term @{text t}
-  after applying a style @{text s} to it (see below).
-
   \item @{text "@{text s}"} prints uninterpreted source text @{text
   s}.  This is particularly useful to print portions of text according
   to the Isabelle document style, without demanding well-formedness,
   e.g.\ small pieces of terms that should not be parsed or
   type-checked yet.

 *}
 
 
 subsubsection {* Styled antiquotations *}
 
-text {* Some antiquotations like @{text thm_style} and @{text
-  term_style} admit an extra \emph{style} specification to modify the
-  printed result.  The following standard styles are available:
+text {* The antiquotations @{text thm}, @{text prop} and @{text
+  term} admit an extra \emph{style} specification to modify the
+  printed result.  A style is specified by a name with a possibly
+  empty number of arguments;  multiple styles can be sequenced with
+  commas.  The following standard styles are available:
 
   \begin{description}
   
   \item @{text lhs} extracts the first argument of any application
   form with at least two arguments --- typically meta-level or

   argument.
   
   \item @{text "concl"} extracts the conclusion @{text C} from a rule
   in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
   
-  \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number
-  @{text "1, \<dots>, 9"}, respectively, from from a rule in Horn-clause
+  \item @{text "prem"} @{text n} extract premise number
+  @{text "n"} from from a rule in Horn-clause
   normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
 
   \end{description}
 *}