NEWS
changeset 21717 410ca6910f6f
parent 21647 fccafa917a68
child 21735 0c65e072f4be
     1.1 --- a/NEWS	Sat Dec 09 18:05:34 2006 +0100
     1.2 +++ b/NEWS	Sat Dec 09 18:05:36 2006 +0100
     1.3 @@ -45,13 +45,18 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* Added antiquotation @{theory name} which prints the name $A$, after
     1.8 -checking that it refers to a valid ancestor theory in the current
     1.9 -context.
    1.10 +* Added antiquotation @{theory name} which prints the given name,
    1.11 +after checking that it refers to a valid ancestor theory in the
    1.12 +current context.
    1.13  
    1.14  * Added antiquotations @{ML_type text} and @{ML_struct text} which
    1.15  check the given source text as ML type/structure, printing verbatim.
    1.16  
    1.17 +* Added antiquotation @{abbrev "c args"} which prints the abbreviation
    1.18 +"c args == rhs" given in the current context.  (Any number of
    1.19 +arguments on the LHS may be given.)
    1.20 +
    1.21 +
    1.22  
    1.23  *** Pure ***
    1.24