author | wenzelm |
Tue, 04 Jul 2006 21:26:26 +0200 | |
changeset 20013 | 57505678692d |
parent 20012 | b62836400a33 |
child 20014 | 729a45534001 |
--- 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"