NEWS

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