# HG changeset patch
# User wenzelm
# Date 1129911417 -7200
# Node ID 2602be0d99aeadde1a3d4d3ebed13fc2099ad314
# Parent  788836292b1a684e6b1d10ce8dbbc0f1c5a9716b
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
 * Internal goals: structure Goal.

diff -r 788836292b1a -r 2602be0d99ae NEWS
--- a/NEWS	Fri Oct 21 18:15:00 2005 +0200
+++ b/NEWS	Fri Oct 21 18:16:57 2005 +0200
@@ -15,9 +15,13 @@
 with Isar theories; migration is usually quite simple with the ML
 function use_legacy_bindings.  INCOMPATIBILITY.
 
-* Legacy goal package: removed former user-level functions top_sg,
-prin, printyp, pprint_term/typ, which tend to cause confusion about
-the actual goal (!) context being used here.
+* Legacy goal package: reduced interface to the bare minimum required
+to keep existing proof scripts running.  Most other user-level
+functions are now part of the OldGoals structure, which is *not* open
+by default (consider isatool expandshort before open OldGoals).
+Removed top_sg, prin, printyp, pprint_term/typ altogether, because
+these tend to cause confusion about the actual goal (!) context being
+used here, which is not necessarily the same as the_context().
 
 * Command 'find_theorems': support "*" wildcard in "name:" criterion.
 
@@ -65,6 +69,12 @@
 
 *** ML ***
 
+* Internal goals: 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).
+
 * 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