--- 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