NEWS

--- a/NEWS	Tue Jul 04 21:22:53 2006 +0200
+++ b/NEWS	Tue Jul 04 21:26:26 2006 +0200
@@ -85,6 +85,9 @@
   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: 'print_facts' prints all local facts of the current context,
+both named and unnamed ones.
+
 * Isar: 'def' now admits simultaneous definitions, e.g.:
 
   def x == "t" and y == "u"