# HG changeset patch
# User wenzelm
# Date 1136332852 -3600
# Node ID ecdd71518f335b3f5945da1286a8b9c6a710b0e7
# Parent  20dd2f7dca4b9595c6c26cca51eb7ca143819a12
* Pure/Isar: Toplevel.theory_theory_to_proof;

diff -r 20dd2f7dca4b -r ecdd71518f33 NEWS
--- a/NEWS	Wed Jan 04 00:52:49 2006 +0100
+++ b/NEWS	Wed Jan 04 01:00:52 2006 +0100
@@ -279,12 +279,16 @@
 slightly more general idea of ``protecting'' meta-level rule
 statements.
 
-* Pure/goals: structure Goal provides simple interfaces for
+* Pure: structure Goal provides simple interfaces for
 init/conclude/finish and tactical prove operations (replacing former
 Tactic.prove).  Note that OldGoals.prove_goalw_cterm has long been
 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, i.e. the 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
 very context that the initial simpset has been retrieved from (by