1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Wed Oct 07 16:57:56 2009 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Oct 08 15:16:13 2009 +0200
     1.3 @@ -145,8 +145,6 @@
     1.4      @{antiquotation_def abbrev} & : & @{text antiquotation} \\
     1.5      @{antiquotation_def typeof} & : & @{text antiquotation} \\
     1.6      @{antiquotation_def typ} & : & @{text antiquotation} \\
     1.7 -    @{antiquotation_def thm_style} & : & @{text antiquotation} \\
     1.8 -    @{antiquotation_def term_style} & : & @{text antiquotation} \\
     1.9      @{antiquotation_def "text"} & : & @{text antiquotation} \\
    1.10      @{antiquotation_def goals} & : & @{text antiquotation} \\
    1.11      @{antiquotation_def subgoals} & : & @{text antiquotation} \\
    1.12 @@ -182,16 +180,14 @@
    1.13  
    1.14      antiquotation:
    1.15        'theory' options name |
    1.16 -      'thm' options thmrefs |
    1.17 +      'thm' options styles thmrefs |
    1.18        'lemma' options prop 'by' method |
    1.19 -      'prop' options prop |
    1.20 -      'term' options term |
    1.21 +      'prop' options styles prop |
    1.22 +      'term' options styles term |
    1.23        'const' options term |
    1.24        'abbrev' options term |
    1.25        'typeof' options term |
    1.26        'typ' options type |
    1.27 -      'thm\_style' options name thmref |
    1.28 -      'term\_style' options name term |
    1.29        'text' options name |
    1.30        'goals' options |
    1.31        'subgoals' options |
    1.32 @@ -205,6 +201,10 @@
    1.33      ;
    1.34      option: name | name '=' name
    1.35      ;
    1.36 +    styles: '(' (style * ',') ')'
    1.37 +    ;
    1.38 +    style: (name *)
    1.39 +    ;
    1.40    \end{rail}
    1.41  
    1.42    Note that the syntax of antiquotations may \emph{not} include source
    1.43 @@ -241,12 +241,6 @@
    1.44  
    1.45    \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
    1.46    
    1.47 -  \item @{text "@{thm_style s a}"} prints theorem @{text a},
    1.48 -  previously applying a style @{text s} to it (see below).
    1.49 -  
    1.50 -  \item @{text "@{term_style s t}"} prints a well-typed term @{text t}
    1.51 -  after applying a style @{text s} to it (see below).
    1.52 -
    1.53    \item @{text "@{text s}"} prints uninterpreted source text @{text
    1.54    s}.  This is particularly useful to print portions of text according
    1.55    to the Isabelle document style, without demanding well-formedness,
    1.56 @@ -285,9 +279,11 @@
    1.57  
    1.58  subsubsection {* Styled antiquotations *}
    1.59  
    1.60 -text {* Some antiquotations like @{text thm_style} and @{text
    1.61 -  term_style} admit an extra \emph{style} specification to modify the
    1.62 -  printed result.  The following standard styles are available:
    1.63 +text {* The antiquotations @{text thm}, @{text prop} and @{text
    1.64 +  term} admit an extra \emph{style} specification to modify the
    1.65 +  printed result.  A style is specified by a name with a possibly
    1.66 +  empty number of arguments;  multiple styles can be sequenced with
    1.67 +  commas.  The following standard styles are available:
    1.68  
    1.69    \begin{description}
    1.70    
    1.71 @@ -301,8 +297,8 @@
    1.72    \item @{text "concl"} extracts the conclusion @{text C} from a rule
    1.73    in Horn-clause normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}.
    1.74    
    1.75 -  \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number
    1.76 -  @{text "1, \<dots>, 9"}, respectively, from from a rule in Horn-clause
    1.77 +  \item @{text "prem"} @{text n} extract premise number
    1.78 +  @{text "n"} from from a rule in Horn-clause
    1.79    normal form @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> C"}
    1.80  
    1.81    \end{description}