1.1 --- a/NEWS	Wed Nov 30 21:51:23 2005 +0100
     1.2 +++ b/NEWS	Wed Nov 30 22:52:46 2005 +0100
     1.3 @@ -61,6 +61,10 @@
     1.4    have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
     1.5    have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
     1.6  
     1.7 +* Isar: 'def' now admits simultaneous definitions, e.g.:
     1.8 +
     1.9 +  def x == "t" and y == "u"
    1.10 +
    1.11  * Provers/induct: improved internal context management to support
    1.12  local fixes and defines on-the-fly.  Thus explicit meta-level
    1.13  connectives !! and ==> are rarely required anymore in inductive goals