--- a/NEWS Thu Jan 05 22:30:00 2006 +0100
+++ b/NEWS Fri Jan 06 15:18:19 2006 +0100
@@ -285,9 +285,10 @@
obsolete, it is ill-behaved in a local proof context (e.g. with local
fixes/assumes or in a locale context).
-* Pure/Isar: Toplevel.theory_theory_to_proof admits transactions that
-modify the theory before entering a proof state (essentially an atomic
-composition of Toplevel.theory and Toplevel.theory_to_proof).
+* Pure/Isar: Toplevel.theory_to_proof admits transactions that modify
+the theory before entering a proof state. Transactions now always see
+a quasi-functional intermediate checkpoint, both in interactive and
+batch mode.
* Simplifier: the simpset of a running simplification process now
contains a proof context (cf. Simplifier.the_context), which is the