NEWS

 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9'
 to print the specified premise.  TermStyle.add_style provides an ML
 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 ***
 
 * Considerably improved version of 'constdefs' command.  Now performs
 automatic type-inference of declared constants; additional support for

 * New syntax 'name(i-j, i-, i, ...)' for referring to specific
 selections of theorems in named facts via index ranges.
 
 * 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 ***
 
 * New commands for the interpretation of locale expressions in theories (1),