# HG changeset patch
# User wenzelm
# Date 1136333099 -3600
# Node ID 0728c4c38b6239e4d5a55c13722505ab918a48ef
# Parent  ecdd71518f335b3f5945da1286a8b9c6a710b0e7
tuned;

diff -r ecdd71518f33 -r 0728c4c38b62 NEWS
--- a/NEWS	Wed Jan 04 01:00:52 2006 +0100
+++ b/NEWS	Wed Jan 04 01:04:59 2006 +0100
@@ -286,8 +286,8 @@
 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, i.e. the composition
-of Toplevel.theory and Toplevel.theory_to_proof.
+modify the theory before entering a proof state (essentially an atomic
+composition of Toplevel.theory and Toplevel.theory_to_proof).
 
 * Simplifier: the simpset of a running simplification process now
 contains a proof context (cf. Simplifier.the_context), which is the