Isar: 'print_facts' prints all local facts;
authorwenzelm
Tue, 04 Jul 2006 21:26:26 +0200
changeset 20013 57505678692d
parent 20012 b62836400a33
child 20014 729a45534001
Isar: 'print_facts' prints all local facts;
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"