NEWS
changeset 30530 03c120763ea8
parent 30461 00323c45ea83
child 30539 c96c72709a20
     1.1 --- a/NEWS	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/NEWS	Sun Mar 15 15:59:45 2009 +0100
     1.3 @@ -603,6 +603,9 @@
     1.4  delicate details of mutexes and condition variables.  [Poly/ML 5.2.1
     1.5  or later]
     1.6  
     1.7 +* Simplified ML attribute and method setup, cf. functions Attrib.setup
     1.8 +and Method.setup, as well as commands 'attribute_setup'.
     1.9 +
    1.10  * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
    1.11  to 'a -> thm, while results are always tagged with an authentic oracle
    1.12  name.  The Isar command 'oracle' is now polymorphic, no argument type