NEWS
changeset 61653 71da80a379c6
parent 61629 90f54d9e63f2
child 61658 5dce70aecbfc
     1.1 --- a/NEWS	Wed Nov 11 19:22:18 2015 +0100
     1.2 +++ b/NEWS	Thu Nov 12 11:30:56 2015 +0100
     1.3 @@ -92,7 +92,8 @@
     1.4  symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
     1.5  
     1.6  * Antiquotation @{theory_text} prints uninterpreted theory source text
     1.7 -(outer syntax with command keywords etc.).
     1.8 +(outer syntax with command keywords etc.). This may be used in the short
     1.9 +form \<^theory_text>\<open>...\<close>.
    1.10  
    1.11  * Antiquotations @{command}, @{method}, @{attribute} print checked
    1.12  entities of the Isar language.
    1.13 @@ -133,11 +134,11 @@
    1.14  the lack of the surrounding isabelle markup environment in output.
    1.15  
    1.16  * Document antiquotations @{emph} and @{bold} output LaTeX source
    1.17 -recursively, adding appropriate text style markup. These are typically
    1.18 -used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
    1.19 +recursively, adding appropriate text style markup. These may be used in
    1.20 +the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
    1.21  
    1.22  * Document antiquotation @{footnote} outputs LaTeX source recursively,
    1.23 -marked as \footnote{}. This is typically used in the short form \<^footnote>\<open>...\<close>.
    1.24 +marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.
    1.25  
    1.26  
    1.27  *** Isar ***