* Pure/Isar: Toplevel.theory_theory_to_proof;
Wed, 04 Jan 2006 01:00:52 +0100
changeset 18567 ecdd71518f33
parent 18566 20dd2f7dca4b
child 18568 0728c4c38b62
* Pure/Isar: Toplevel.theory_theory_to_proof;
--- 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
-* 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