--- a/NEWS Wed Aug 17 17:04:15 2005 +0200
+++ b/NEWS Thu Aug 18 11:17:32 2005 +0200
@@ -90,6 +90,12 @@
interface for introducing further styles. See also the "LaTeX Sugar"
document practical applications.
+* Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
+a proof context.
+
+* Proper output of antiquotations for theory commands involving a
+proof context (such as 'locale' or 'theorem (in loc) ...').
+
*** Pure ***
@@ -187,6 +193,10 @@
* More efficient treatment of intermediate checkpoints in interactive
theory development.
+* 'print_theorems': in theory mode, really print the difference
+wrt. the last state (works for interactive theory development only),
+in proof mode print all local facts (cf. 'print_facts');
+
*** Locales ***