# HG changeset patch
# User wenzelm
# Date 1152041186 -7200
# Node ID 57505678692d6737d3c25c25d3ae524e568f83e9
# Parent  b62836400a33fc277462cf62012b72b01df60d2b
Isar: 'print_facts' prints all local facts;

diff -r b62836400a33 -r 57505678692d 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"