1.1 --- a/NEWS	Fri Oct 21 18:15:00 2005 +0200
     1.2 +++ b/NEWS	Fri Oct 21 18:16:57 2005 +0200
     1.3 @@ -15,9 +15,13 @@
     1.4  with Isar theories; migration is usually quite simple with the ML
     1.5  function use_legacy_bindings.  INCOMPATIBILITY.
     1.6  
     1.7 -* Legacy goal package: removed former user-level functions top_sg,
     1.8 -prin, printyp, pprint_term/typ, which tend to cause confusion about
     1.9 -the actual goal (!) context being used here.
    1.10 +* Legacy goal package: reduced interface to the bare minimum required
    1.11 +to keep existing proof scripts running.  Most other user-level
    1.12 +functions are now part of the OldGoals structure, which is *not* open
    1.13 +by default (consider isatool expandshort before open OldGoals).
    1.14 +Removed top_sg, prin, printyp, pprint_term/typ altogether, because
    1.15 +these tend to cause confusion about the actual goal (!) context being
    1.16 +used here, which is not necessarily the same as the_context().
    1.17  
    1.18  * Command 'find_theorems': support "*" wildcard in "name:" criterion.
    1.19  
    1.20 @@ -65,6 +69,12 @@
    1.21  
    1.22  *** ML ***
    1.23  
    1.24 +* Internal goals: structure Goal provides simple interfaces for
    1.25 +init/conclude/finish and tactical prove operations (replacing former
    1.26 +Tactic.prove).  Note that OldGoals.prove_goalw_cterm has long been
    1.27 +obsolete, it is ill-behaved in a local proof context (e.g. with local
    1.28 +fixes/assumes or in a locale context).
    1.29 +
    1.30  * Simplifier: the simpset of a running simplification process now
    1.31  contains a proof context (cf. Simplifier.the_context), which is the
    1.32  very context that the initial simpset has been retrieved from (by