# HG changeset patch
# User wenzelm
# Date 1124356652 -7200
# Node ID 78f1b66f70a4895feac7ad296a72b72fc9c62a54
# Parent  8327b71282cee92508b50b0e47e74e4e9d0734b6
* Proper output of proof terms within a proof context;
* Proper output of antiquotations for theory commands involving a proof context;
* 'print_theorems': in theory mode print difference of facts, in proof mode print local facts;

diff -r 8327b71282ce -r 78f1b66f70a4 NEWS
--- 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 ***